From 82158ca606625eaaf3aa4f516caeee61423154bd Mon Sep 17 00:00:00 2001 From: Lucas Tabary-Maujean Date: Tue, 17 Jun 2025 17:46:47 +0200 Subject: [PATCH] feat: new source-documented lazy/eager logic. This logic is deliberately slightly less expressive than the one it replaces, which does not hinder usability in any cryptographic context, with the hope that it is simpler to maintain and verify. --- examples/PRG.ec | 12 +- examples/UC/RndO.ec | 3 +- src/ecEnv.ml | 5 +- src/ecHiTacticals.ml | 3 +- src/ecParser.mly | 20 +- src/ecParsetree.ml | 14 +- src/phl/ecPhlEager.ml | 864 +++++++++++++------------------- src/phl/ecPhlEager.mli | 180 +++---- theories/crypto/PROM.ec | 3 +- theories/distributions/SDist.ec | 13 +- 10 files changed, 465 insertions(+), 652 deletions(-) diff --git a/examples/PRG.ec b/examples/PRG.ec index f32ddf910b..870a3ce0eb 100644 --- a/examples/PRG.ec +++ b/examples/PRG.ec @@ -340,11 +340,8 @@ section. by wp; rnd; wp; rnd{2}; auto; rewrite dseed_ll. (* presampling ~ postsampling *) seq 2 2: (={glob A, glob F, glob Plog}); first by sim. - eager (H: Resample.resample(); ~ Resample.resample(); - : ={glob Plog} ==> ={glob Plog}) - : (={glob A, glob Plog, glob F})=> //; - first by sim. - eager proc H (={glob Plog, glob F})=> //. + eager call (: ={glob Plog, glob A, glob F}). + eager proc (={glob Plog, glob F}) => //; try sim. + eager proc; inline Resample.resample. swap{1} 3 3. swap{2} [4..5] 2. swap{2} [6..8] 1. swap{1} 4 3. swap{1} 4 2. swap{2} 2 4. @@ -357,10 +354,9 @@ section. by wp; rnd{2}; auto=> />; smt (size_ge0). rcondt{2} 1; first by move=> &hr; auto=> /#. rcondf{2} 3; first by move=> &hr; auto=> /#. - + by sim. - + by sim. + by sim. + by eager proc; swap{1} 1 4; sim. - by sim. + by auto. qed. lemma P_PrgI &m: diff --git a/examples/UC/RndO.ec b/examples/UC/RndO.ec index 2450f14fbb..e7b3c09838 100644 --- a/examples/UC/RndO.ec +++ b/examples/UC/RndO.ec @@ -681,8 +681,7 @@ lemma eager_D : D(RRO).distinguish, RRO.resample(); : ={glob D, FRO.m} ==> ={FRO.m, glob D} /\ ={res}]. proof. - eager proc (H_: RRO.resample(); ~ RRO.resample();: ={FRO.m} ==> ={FRO.m}) - (={FRO.m}) =>//; try by sim. + eager proc (={FRO.m}) => //; try by sim. + by apply eager_init. + by apply eager_get. + by apply eager_set. + by apply eager_rem. + by apply eager_sample. + by apply eager_in_dom. + by apply eager_restrK. diff --git a/src/ecEnv.ml b/src/ecEnv.ml index a4a5c8a7ca..4ccfcc7ae8 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -2360,7 +2360,7 @@ module NormMp = struct match item with | MI_Module me -> mod_use env rm fdone us (EcPath.mqname mp me.me_name) | MI_Variable v -> add_var env (xpath mp v.v_name) us - | MI_Function f -> fun_use_aux env rm fdone us (xpath mp f.f_name) + | MI_Function f -> gen_fun_use env fdone rm us (xpath mp f.f_name) and body_use env rm fdone mp us comps body = match body with @@ -2372,9 +2372,6 @@ module NormMp = struct | ME_Structure ms -> List.fold_left (item_use env rm fdone mp) us ms.ms_body - and fun_use_aux env rm fdone us f = - gen_fun_use env fdone rm us f - let mod_use_top env mp = let mp = norm_mpath env mp in let me, _ = Mod.by_mpath mp env in diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 9eb6521e35..45af108525 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -223,9 +223,8 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Peager_if -> EcPhlEager.process_if | Peager_while info -> EcPhlEager.process_while info | Peager_fun_def -> EcPhlEager.process_fun_def - | Peager_fun_abs infos -> curry EcPhlEager.process_fun_abs infos + | Peager_fun_abs infos -> EcPhlEager.process_fun_abs infos | Peager_call info -> EcPhlEager.process_call info - | Peager infos -> curry EcPhlEager.process_eager infos | Pbd_equiv (nm, f1, f2) -> EcPhlConseq.process_bd_equiv nm (f1, f2) | Pauto -> EcPhlAuto.t_auto ~conv:`Conv | Plossless -> EcPhlHiAuto.t_lossless diff --git a/src/ecParser.mly b/src/ecParser.mly index eb1a1a9801..e53e1a7f17 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2845,35 +2845,25 @@ logtactic: | WLOG b=boption(SUFF) COLON ids=loc(ipcore_name)* SLASH f=form { Pwlog (ids, b, f) } -eager_info: -| h=ident - { LE_done h } - -| LPAREN h=ident COLON s1=stmt TILD s2=stmt COLON pr=form LONGARROW po=form RPAREN - { LE_todo (h, s1, s2, pr, po) } - eager_tac: -| SEQ n1=codepos1 n2=codepos1 i=eager_info COLON p=sform - { Peager_seq (i, (n1, n2), p) } +| SEQ n1=codepos1 n2=codepos1 COLON s=stmt COLON p=form_or_double_form + { Peager_seq ((n1, n2), s, p) } | IF { Peager_if } -| WHILE i=eager_info +| WHILE i=sform { Peager_while i } | PROC { Peager_fun_def } -| PROC i=eager_info f=sform - { Peager_fun_abs (i, f) } +| PROC f=sform + { Peager_fun_abs f } | CALL info=gpterm(call_info) { Peager_call info } -| info=eager_info COLON p=sform - { Peager (info, p) } - form_or_double_form: | f=sform { Single f } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index b438cc9046..8624dad56f 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -596,11 +596,6 @@ type trans_formula = type trans_info = trans_kind * trans_formula -(* -------------------------------------------------------------------- *) -type eager_info = - | LE_done of psymbol - | LE_todo of psymbol * pstmt * pstmt * pformula * pformula - (* -------------------------------------------------------------------- *) type bdh_split = | BDH_split_bop of pformula * pformula * pformula option @@ -776,13 +771,12 @@ type phltactic = (* Eager *) - | Peager_seq of (eager_info * pcodepos1 pair * pformula) + | Peager_seq of (pcodepos1 pair * pstmt * pformula doption) | Peager_if - | Peager_while of (eager_info) + | Peager_while of pformula | Peager_fun_def - | Peager_fun_abs of (eager_info * pformula) - | Peager_call of (call_info gppterm) - | Peager of (eager_info * pformula) + | Peager_fun_abs of pformula + | Peager_call of call_info gppterm (* Relation between logic *) | Pbd_equiv of (side * pformula * pformula) diff --git a/src/phl/ecPhlEager.ml b/src/phl/ecPhlEager.ml index a99092c829..30b589493d 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -1,299 +1,358 @@ -(* -------------------------------------------------------------------- *) -open EcUtils -open EcLocation open EcAst -open EcTypes -open EcModules -open EcFol -open EcEnv -open EcPV - open EcCoreGoal +open EcEnv +open EcFol open EcLowGoal open EcLowPhlGoal - -module ER = EcReduction -module PT = EcProofTerm +open EcMatching.Zipper +open EcModules +open EcPV +open EcTypes +open EcUtils +module ER = EcReduction +module PT = EcProofTerm module TTC = EcProofTyping -(* -------------------------------------------------------------------- *) -let pf_destr_eqobsS pf env f = - let es = destr_equivS f in - let of_form = - try Mpv2.of_form env - with Not_found -> tc_error pf "cannot reconize a set of equalities" +(** Builds a formula that represents equality on the list of variables [l] + between two memories [ml] and [mr] *) +let list_eq_to_form ml mr (l, l_glob) = + let to_form m = List.map (fun (pv, ty) -> (f_pvar pv ty m).inv) in + let to_form_glob m = + List.map (fun x -> (f_glob (EcPath.mget_ident x) m).inv) in - (es, es.es_sl, es.es_sr, of_form (es_pr es), of_form (es_po es)) - -(* -------------------------------------------------------------------- *) -let pf_hSS pf hyps h = - let tH = LDecl.hyp_by_id h hyps in - (tH, pf_destr_eqobsS pf (LDecl.toenv hyps) tH) - -(* -------------------------------------------------------------------- *) -let tc1_destr_eagerS tc s s' = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let c , c' = es.es_sl, es.es_sr in - let s1, c = s_split env (Zpr.cpos (List.length s.s_node)) c in - let c',s1' = s_split env (Zpr.cpos (List.length c'.s_node - List.length s'.s_node)) c' in - - if not (List.all2 i_equal s1 s.s_node) then begin - let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in + { + ml; + mr; + inv = + f_eqs + (to_form ml l @ to_form_glob ml l_glob) + (to_form mr l @ to_form_glob mr l_glob); + } + +(** Returns a formula that describes equality on all variables from one side of + the memory present in the formula [q]. + + Example: If [q] is [(a{ml} \/ b{m'} /\ c{ml})], (with [ml] the first bound + memory, [mr] the second and [m'] another memory, distinct from [ml]) then + this function returns [(a{ml} = a{mr} /\ c{ml} = c{mr})]. The result of this + operation is sometimes denoted [={q.m1}]. *) +let eq_on_sided_form env { ml; mr; inv } = + PV.fv env ml inv |> PV.elements |> list_eq_to_form ml mr + +(** Returns a formula that describes equality on all variables from both + memories in predicate [inv], as well as equality on all variables read from + [c]. + + This is used to implement what is denoted [Eq] in the module documentation, + i.e. equality on the whole memory. *) +let eq_on_form_and_stmt env { ml; mr; inv } c = + s_read env c + |> PV.union (PV.fv env ml inv) + |> PV.union (PV.fv env mr inv) + |> PV.elements |> list_eq_to_form ml mr + +(** Equality on all variables from a function [f] *) +let eq_on_fun env m1 m2 f = + let l, l' = NormMp.flatten_use (NormMp.fun_use env f) in + let l_glob = List.map EcPath.mident l in + let l_pv = List.map (fun (x, ty) -> (pv_glob x, ty)) l' in + list_eq_to_form m1 m2 (l_pv, l_glob) + +(** Given a goal environment [tc] and a statement [s], if the goal is an + equivalence of the shape [s; c ~ c'; s], returns the same equivalence goal, + as well as the terms c and c'. + + Yields an error if the statements are not of the right form. *) +let destruct_eager tc s = + let env = FApi.tc1_env tc + and es = tc1_as_equivS tc + and ss = List.length s.s_node in + + let c, c' = (es.es_sl, es.es_sr) in + let z, c = s_split env (Zpr.cpos ss) c + and c', z' = s_split env (Zpr.cpos (List.length c'.s_node - ss)) c' in + + let env, _, _ = FApi.tc1_eflat tc in + let z_eq_s = ER.EqTest.for_stmt env (stmt z) s + and z'_eq_s = ER.EqTest.for_stmt env (stmt z') s in + + if z_eq_s && z'_eq_s then (es, stmt c, stmt c') + else + let err_stmt, prefix = + if z_eq_s then (z', "tail of the right") else (z, "head of the left") + and ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in tc_error_lazy !!tc (fun fmt -> - Format.fprintf fmt - "the head of the left statement is not of the right form:@\n%a should be@\n%a" - (EcPrinting.pp_stmt ppe) (stmt s1) (EcPrinting.pp_stmt ppe) s) - end; - - if not (List.all2 i_equal s1' s'.s_node) then begin - let ppe = EcPrinting.PPEnv.ofenv (FApi.tc1_env tc) in - tc_error_lazy !!tc (fun fmt -> - Format.fprintf fmt - "the tail of the right statement is not of the right form:@\n%a should be@\n%a" - (EcPrinting.pp_stmt ppe) (stmt s1') (EcPrinting.pp_stmt ppe) s') - end; - - (es, stmt c, stmt c') - -(* -------------------------------------------------------------------- *) -(* This ensure condition (d) and (e) of the eager_seq rule. *) -let pf_compat pf env modS modS' eqR eqIs eqXs = - if not (Mpv2.subset eqIs eqR) then begin - let ml, mr = EcIdent.create "&1_dummy", EcIdent.create "&2_dummy" in - let f_true = {ml; mr; inv=f_true} in - let eqR = Mpv2.to_form_ts_inv eqR f_true in - let eqIs = Mpv2.to_form_ts_inv eqIs f_true in - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "%a should be included in %a" - (EcPrinting.pp_form ppe) eqIs.inv (EcPrinting.pp_form ppe) eqR.inv) - end; - - let check_pv x1 x2 _ = - if not (Mpv2.mem x1 x2 eqXs) - && (PV.mem_pv env x1 modS || PV.mem_pv env x2 modS') - then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in Format.fprintf fmt - "equality of %a and %a should be ensured by the swapping statement" - (EcPrinting.pp_pv ppe) x1 (EcPrinting.pp_pv ppe) x2) + "eager: the %s statement is not of the right form:@\n\ + %a should be@\n\ + %a" + prefix (EcPrinting.pp_stmt ppe) (stmt err_stmt) + (EcPrinting.pp_stmt ppe) s) + +(** Given a goal environment with a current goal of the shape [s; op ~ op'; s], + returns the triplet [(es, s, op, op')]. Yields an error if the goal doesn't + have the right shape *) +let destruct_on_op id_op tc = + let env = FApi.tc1_env tc and es = tc1_as_equivS tc in + let s = + try + let s, _ = split_at_cpos1 env (-1, `ByMatch (None, id_op)) es.es_sl + (* ensure the right statement also contains an [id_op]: *) + and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in + s + with InvalidCPos -> + tc_error_lazy !!tc (fun fmt -> + Format.fprintf fmt "eager: invalid pivot statement") + in - and check_glob m = - if not (Mpv2.mem_glob m eqXs) - && (PV.mem_glob env m modS || PV.mem_glob env m modS') - then + if List.is_empty s then + tc_error_lazy !!tc (fun fmt -> + Format.fprintf fmt "eager: empty swapping statement"); + + let es, c1, c2 = destruct_eager tc (stmt s) in + match (c1.s_node, c2.s_node) with + | [ i1 ], [ i2 ] -> (es, stmt s, i1, i2) + | _, _ -> + let verb, side = + if List.length c1.s_node = 1 then ("precede", "right") + else ("follow", "left") + in + tc_error_lazy !!tc (fun fmt -> + Format.fprintf fmt + "eager: no statements may %s the %s pivot statement." verb side) + +let rec match_eq tc m1 m2 t1 t2 = + match (t1.f_node, t2.f_node) with + | Fpvar (p1, m1_), Fpvar (p2, m2_) -> + ((m1 = m1_ && m2 = m2_) || (m1 = m2_ && m2 = m1_)) && p1 = p2 + | Fglob (p1, m1_), Fglob (p2, m2_) -> + ((m1 = m1_ && m2 = m2_) || (m1 = m2_ && m2 = m1_)) && p1 = p2 + | Ftuple l1, Ftuple l2 -> List.for_all2 (match_eq tc m1 m2) l1 l2 + | _ -> false + +(** Ensure that a given proposition is a conjunction of same-name variables + equalities between two given memories. + + This test is of course a bit conservative but should be sufficient for all + the use cases it covers *) +let rec ensure_eq_shape tc m1 m2 q = + match q.f_node with + | Fapp (_, [ q1; q2 ]) when is_and q -> + ensure_eq_shape tc m1 m2 q1 && ensure_eq_shape tc m1 m2 q2 + | Fapp (_, [ t1; t2 ]) when is_eq q -> match_eq tc m1 m2 t1 t2 + | _ -> is_true q + +(** Ensure the swapping statement [s] only interacts with global variables. *) +let check_only_global pf env s = + let sw = s_write env s + and sr = s_read env s + and check_mp _ = () + and check_glob v _ = + if is_loc v then tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "equality of %a should be ensured by the swapping statement" - (EcPrinting.pp_topmod ppe) m) - + let ppe = EcPrinting.PPEnv.ofenv env in + Format.fprintf fmt + "eager: swapping statement may use only global variables: %a" + (EcPrinting.pp_pv ppe) v) in - Mpv2.iter check_pv check_glob eqR + PV.iter check_glob check_mp sw; + PV.iter check_glob check_mp sr (* -------------------------------------------------------------------- *) -let t_eager_seq_r i j eqR h tc = - let env, hyps, _ = FApi.tc1_eflat tc in - - (* h is a proof of (h) *) - let tH, (_, s, s', eqIs, eqXs) = pf_hSS !!tc hyps h in - let eC, c, c' = tc1_destr_eagerS tc s s' in - let seqR = Mpv2.of_form env eqR in - - (* check (d) and (e) *) - pf_compat !!tc env (s_write env s) (s_write env s') seqR eqIs eqXs; - - let eqO2 = Mpv2.eq_refl (PV.fv env (fst eC.es_mr) (es_po eC).inv) in - let c1 ,c2 = s_split env i c in - let c1',c2' = s_split env j c' in - - let to_form eq = Mpv2.to_form_ts_inv eq {ml=(fst eC.es_ml); mr=(fst eC.es_mr); inv=f_true} in - - let a = f_equivS (snd eC.es_ml) (snd eC.es_mr) (es_pr eC) (stmt (s.s_node@c1)) (stmt (c1'@s'.s_node)) eqR - and b = f_equivS (snd eC.es_ml) (snd eC.es_mr) eqR (stmt (s.s_node@c2)) (stmt (c2'@s'.s_node)) (es_po eC) - and c = f_equivS (snd eC.es_mr) (snd eC.es_mr) (to_form (Mpv2.eq_fv2 seqR)) - (stmt c2') (stmt c2') (to_form eqO2) in - - FApi.t_first - (t_apply_hyp h) - (FApi.xmutate1 tc `EagerSeq [tH; a; b; c]) +(* Internal variants of eager tactics *) + +let t_eager_seq_r (i, j) s (r2, r1) tc = + let env, _, _ = FApi.tc1_eflat tc and eC, c, c' = destruct_eager tc s in + + let (_, ml_ty), (_, mr_ty) = (eC.es_ml, eC.es_mr) in + let c1, c2 = s_split env i c and c1', c2' = s_split env j c' in + let eqMem1 = eq_on_form_and_stmt env r1 (stmt c1') + and eqQ1 = eq_on_sided_form env (es_po eC) in + + let a = + f_equivS ml_ty mr_ty (es_pr eC) + (stmt (s.s_node @ c1)) + (stmt (c1' @ s.s_node)) + r2 + and b = + f_equivS ml_ty mr_ty r1 + (stmt (s.s_node @ c2)) + (stmt (c2' @ s.s_node)) + (es_po eC) + and c = f_equivS mr_ty mr_ty eqMem1 (stmt c1') (stmt c1') r1 + and d = f_equivS ml_ty ml_ty r2 (stmt c2) (stmt c2) eqQ1 in + FApi.xmutate1 tc `EagerSeq [ a; b; c; d ] (* -------------------------------------------------------------------- *) let t_eager_if_r tc = - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - - let (e , c1 , c2 ), s = pf_last_if !!tc es.es_sl in - let (e', c1', c2'), s' = pf_first_if !!tc es.es_sr in + let es, s, c, c' = destruct_on_op `If tc in + let e, c1, c2 = destr_if c and e', c1', c2' = destr_if c' in - let fel = ss_inv_generalize_right (ss_inv_of_expr ml e) mr in - let fer = ss_inv_generalize_left (ss_inv_of_expr mr e') ml in + let { ml; mr; inv = pr_inv } = es_pr es in + let { es_ml = _, ml_ty; es_mr = _, mr_ty } = es in + let fe = (ss_inv_of_expr ml e).inv and fe' = (ss_inv_of_expr mr e').inv in let aT = - EcSubst.f_forall_mems_ts_inv es.es_ml es.es_mr - (map_ts_inv2 f_imp (es_pr es) (map_ts_inv2 f_eq fel fer)) in + f_forall + [ (ml, GTmem ml_ty); (mr, GTmem mr_ty) ] + (f_imp pr_inv (f_eq fe fe')) + in let bT = - let b = EcIdent.create "b1" in - let fe = ss_inv_generalize_right (ss_inv_of_expr ml e) mr in - let eqb = map_ts_inv2 f_eq fe {ml;mr;inv=f_local b tbool} in - - EcSubst.f_forall_mems_ss_inv es.es_mr - (map_ss_inv1 - (f_forall [(b, GTty tbool)]) - (ts_inv_lower_left2 (fun pr po -> f_hoareS (snd es.es_ml) pr s po) (map_ts_inv2 f_and (es_pr es) eqb) eqb)) in + let b = EcIdent.create "b" in + let eqb = f_eq fe (f_local b tbool) in + let pre = { m = ml; inv = f_and pr_inv eqb } in + let post = { m = ml; inv = eqb } in + f_forall [ (mr, GTmem mr_ty); (b, GTty tbool) ] (f_hoareS ml_ty pre s post) + in let cT = - let pre = map_ts_inv2 f_and (es_pr es) (map_ts_inv2 f_eq fel {ml;mr;inv=f_true}) in - let st = stmt (s.s_node @ c1.s_node) in - let st' = stmt (c1'.s_node @ s'.s_node) in - f_equivS (snd es.es_ml) (snd es.es_mr) pre st st' (es_po es) in + let pre = { ml; mr; inv = f_and pr_inv (f_eq fe f_true) } in + let st = stmt (s.s_node @ c1.s_node) in + let st' = stmt (c1'.s_node @ s.s_node) in + f_equivS ml_ty mr_ty pre st st' (es_po es) + in let dT = - let pre = map_ts_inv2 f_and (es_pr es) (map_ts_inv2 f_eq fel {ml;mr;inv=f_false}) in - let st = stmt (s.s_node @ c2.s_node) in - let st' = stmt (c2'.s_node @ s'.s_node) in - f_equivS (snd es.es_ml) (snd es.es_mr) pre st st' (es_po es) in + let pre = { ml; mr; inv = f_and pr_inv (f_eq fe f_false) } in + let st = stmt (s.s_node @ c2.s_node) in + let st' = stmt (c2'.s_node @ s.s_node) in + f_equivS ml_ty mr_ty pre st st' (es_po es) + in - FApi.xmutate1 tc `EagerIf [aT; bT; cT; dT] + FApi.xmutate1 tc `EagerIf [ aT; bT; cT; dT ] (* -------------------------------------------------------------------- *) -let t_eager_while_r h tc = - let env, hyps, _ = FApi.tc1_eflat tc in +let t_eager_while_r i tc = + let env, _, _ = FApi.tc1_eflat tc in - let tH, (_, s, s', eqIs, eqXs) = pf_hSS !!tc hyps h in - let eC, wc, wc' = tc1_destr_eagerS tc s s' in - let ml, mr = fst eC.es_ml, fst eC.es_mr in + let es, s, w, w' = destruct_on_op `While tc in + let e, c = destr_while w and _e, c' = destr_while w' in - let (e , c ), n = pf_first_while !!tc wc in - let (e', c'), n' = pf_first_while !!tc wc' in - if not (List.is_empty n.s_node && List.is_empty n'.s_node) then - tc_error !!tc "no statements should followed the while loops"; + let { ml; mr; inv = pr_inv } = es_pr es in + let { es_ml = _, ml_ty; es_mr = _, mr_ty } = es in - let to_form eq = Mpv2.to_form_ts_inv eq {ml=(fst eC.es_ml);mr=(fst eC.es_mr);inv=f_true} in - - let eqI = (es_pr eC) in - let seqI = - try - Mpv2.of_form env eqI - with Not_found -> - tc_error_lazy !!tc (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "recognize equalities in %a@." (EcPrinting.pp_form ppe) eqI.inv) + let sub_to_left_mem = + let open EcSubst in + subst_expr (add_memory empty mr ml) in - let eqI2 = to_form (Mpv2.eq_fv2 seqI) in - let e1 = ss_inv_generalize_right (ss_inv_of_expr ml e) mr in - let e2 = ss_inv_generalize_left (ss_inv_of_expr mr e') ml in - let post = Mpv2.to_form_ts_inv (Mpv2.union seqI eqXs) (map_ts_inv1 f_not e1) in - - (* check (e) and (f) *) - pf_compat !!tc env (s_write env s) (s_write env s') seqI eqIs eqXs; - let aT = EcSubst.f_forall_mems_ts_inv eC.es_ml eC.es_mr - (map_ts_inv2 f_imp eqI (map_ts_inv2 f_eq e1 e2)) - - and bT = f_equivS (snd eC.es_ml) (snd eC.es_mr) (map_ts_inv2 f_and_simpl eqI e1) (stmt (s.s_node@c.s_node)) - (stmt (c'.s_node@s'.s_node)) eqI + if (not (e_equal e (sub_to_left_mem _e))) then + tc_error !!tc "eager: both while guards must be syntactically equal"; - and cT = f_equivS (snd eC.es_mr) (snd eC.es_mr) eqI2 c' c' eqI2 - in + let eqMem1 = eq_on_form_and_stmt env i c' and eqI = eq_on_sided_form env i in + + let el = ss_inv_of_expr ml e and er = ss_inv_of_expr mr e in - let tsolve tc = - FApi.t_first - (t_apply_hyp h) - (FApi.xmutate1 tc `EagerWhile [tH; aT; bT; cT]) + let aT = + let and_ = f_and_simpl (f_eq el.inv er.inv) eqI.inv in + f_forall [ (ml, GTmem ml_ty); (mr, GTmem mr_ty) ] (f_imp i.inv and_) + and bT = + let pre = { ml; mr; inv = f_and i.inv el.inv } in + f_equivS ml_ty mr_ty pre + (stmt (s.s_node @ c.s_node)) + (stmt (c'.s_node @ s.s_node)) + i + and cT = + let b = EcIdent.create "b" in + let eqb = f_eq el.inv (f_local b tbool) in + let pre = { m = ml; inv = f_and pr_inv eqb } in + let post = { m = ml; inv = eqb } in + f_forall [ (mr, GTmem mr_ty); (b, GTty tbool) ] (f_hoareS ml_ty pre s post) + and dT = f_equivS ml_ty mr_ty eqMem1 c' c' i + and eT = f_equivS ml_ty mr_ty i c c i + and fT = + f_equivS ml_ty mr_ty { ml; mr; inv = f_and i.inv (f_not el.inv) } s s i in - FApi.t_seqsub - (EcPhlConseq.t_equivS_conseq eqI post) - [t_trivial; t_trivial; tsolve] - tc + FApi.xmutate1 tc `EagerWhile [ aT; bT; cT; dT; eT; fT ] (* -------------------------------------------------------------------- *) let t_eager_fun_def_r tc = let env = FApi.tc1_env tc in - let eg = tc1_as_eagerF tc in - let ml, mr = eg.eg_ml, eg.eg_mr in + let eg = tc1_as_eagerF tc in - let fl, fr = - (NormMp.norm_xfun env eg.eg_fl, - NormMp.norm_xfun env eg.eg_fr) - in + let fl, fr = (NormMp.norm_xfun env eg.eg_fl, NormMp.norm_xfun env eg.eg_fr) in EcPhlFun.check_concrete !!tc env fl; EcPhlFun.check_concrete !!tc env fr; - let (memenvl, (fsigl,fdefl), - memenvr, (fsigr,fdefr), env) = Fun.equivS ml mr fl fr env in + let memenvl, (fsigl, fdefl), memenvr, (fsigr, fdefr), env = + Fun.equivS eg.eg_ml eg.eg_mr fl fr env + in let extend mem fdef = match fdef.f_ret with - | None -> {m=fst mem;inv=f_tt}, mem, fdef.f_body + | None -> (f_tt, mem, fdef.f_body) | Some e -> - let v = { ov_name = Some "result"; ov_type = e.e_ty } in - let mem, s = EcMemory.bind_fresh v mem in - (* oget cannot fail — Some in, Some out *) - let x = EcTypes.pv_loc (oget s.ov_name) in - f_pvar x e.e_ty (fst mem), mem, - s_seq fdef.f_body (stmt [i_asgn(LvVar(x,e.e_ty), e)]) + let v = { ov_name = Some "result"; ov_type = e.e_ty } in + let mem, s = EcMemory.bind_fresh v mem in + (* oget cannot fail — Some in, Some out *) + let x = EcTypes.pv_loc (oget s.ov_name) in + ( (f_pvar x e.e_ty (fst mem)).inv, + mem, + s_seq fdef.f_body (stmt [ i_asgn (LvVar (x, e.e_ty), e) ]) ) in let el, meml, sfl = extend memenvl fdefl in let er, memr, sfr = extend memenvr fdefr in - let ml, mr = EcMemory.memory meml, EcMemory.memory memr in + let ml, mr = (EcMemory.memory meml, EcMemory.memory memr) in let s = PVM.empty in - let s = PVM.add env pv_res ml el.inv s in - let s = PVM.add env pv_res mr er.inv s in + let s = PVM.add env pv_res ml el s in + let s = PVM.add env pv_res mr er s in let post = map_ts_inv1 (PVM.subst env s) (eg_po eg) in let s = PVM.empty in let s = EcPhlFun.subst_pre env fsigl ml s in let s = EcPhlFun.subst_pre env fsigr mr s in let pre = map_ts_inv1 (PVM.subst env s) (eg_pr eg) in - let cond = f_equivS (snd meml) (snd memr) pre (s_seq eg.eg_sl sfl) (s_seq sfr eg.eg_sr) post in + let cond = + f_equivS (snd meml) (snd memr) pre (s_seq eg.eg_sl sfl) (s_seq sfr eg.eg_sr) + post + in - FApi.xmutate1 tc `EagerFunDef [cond] + FApi.xmutate1 tc `EagerFunDef [ cond ] (* -------------------------------------------------------------------- *) -let t_eager_fun_abs_r eqI h tc = - let env, hyps, _ = FApi.tc1_eflat tc in +let t_eager_fun_abs_r i tc = + let env, _, _ = FApi.tc1_eflat tc and eg = tc1_as_eagerF tc in - let tH, (_, s, s', eqIs, eqXs) = pf_hSS !!tc hyps h in - let eg = tc1_as_eagerF tc in + if not (s_equal eg.eg_sl eg.eg_sr) then + tc_error !!tc "eager: both swapping statements must be identical"; - if not (s_equal s eg.eg_sl && s_equal s' eg.eg_sr) then - tc_error !!tc "cannot reconize the swapping statement"; + if not (ensure_eq_shape tc i.ml i.mr i.inv) then + tc_error !!tc + "eager: the invariant must be a conjunction of same-name variable \ + equalities"; - let fl, fr = eg.eg_fl, eg.eg_fr in - let pre, post, sg = - EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fl fr eqI in + let s, fl, fr = (eg.eg_sl, eg.eg_fl, eg.eg_fr) in - let do1 og sg = + let pre, post, sg_e = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fl fr i in + let _, _, sg_f = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fr fr i in + let _, _, sg_g = EcPhlFun.FunAbsLow.equivF_abs_spec !!tc env fl fl i in + + let do_e og = let ef = destr_equivF og in - let torefl f = - Mpv2.to_form_ts_inv - (Mpv2.eq_refl (PV.fv env f.mr f.inv)) - {ml=f.ml;mr=f.mr;inv=f_true} - in - f_eagerF (ef_pr ef) s ef.ef_fl ef.ef_fr s' (ef_po ef) - :: f_equivF (torefl (ef_pr ef)) ef.ef_fr ef.ef_fr (torefl (ef_po ef)) - :: sg + f_eagerF (ef_pr ef) s ef.ef_fl ef.ef_fr s (ef_po ef) in - let sg = List.fold_right do1 sg [] in - let seqI = Mpv2.of_form env eqI in - - (* check (e) and (f)*) - pf_compat !!tc env (s_write env s) (s_write env s') seqI eqIs eqXs; + let do_f og = + let ef = destr_equivF og in - (* TODO : check that S S' do not modify glob A *) - let tactic tc = - FApi.t_first (t_apply_hyp h) - (FApi.xmutate1 tc `EagerFunAbs (tH::sg)) + let eqMem = eq_on_fun env i.ml i.mr ef.ef_fr in + f_equivF (map_ts_inv2 f_and eqMem (ef_pr ef)) ef.ef_fl ef.ef_fl (ef_po ef) in + let sg_e = List.map do_e sg_e and sg_f = List.map do_f sg_f in + + (* Reorder per-oracle goals in order to align with the description *) + let sg = + List.combine sg_e (List.combine sg_f sg_g) + |> List.concat_map (fun (x, (y, z)) -> [ x; y; z ]) + and sg_d = f_equivS EcMemory.abstract_mt EcMemory.abstract_mt i s s i in + + let tactic tc = FApi.xmutate1 tc `EagerFunAbs (sg_d :: sg) in + FApi.t_last tactic (EcPhlConseq.t_eagerF_conseq pre post tc) (* -------------------------------------------------------------------- *) @@ -303,338 +362,111 @@ let t_eager_call_r fpre fpost tc = let fpre = EcSubst.ts_inv_rebind fpre (fst es.es_ml) (fst es.es_mr) in let fpost = EcSubst.ts_inv_rebind fpost (fst es.es_ml) (fst es.es_mr) in - let (lvl, fl, argsl), sl = pf_last_call !!tc es.es_sl in + let (lvl, fl, argsl), sl = pf_last_call !!tc es.es_sl in let (lvr, fr, argsr), sr = pf_first_call !!tc es.es_sr in let swl = s_write env sl in let swr = s_write env sr in let check_a e = - let er = e_read env e in + let er = e_read env e in let diff = PV.interdep env swl er in if not (PV.is_empty diff) then tc_error_lazy !!tc (fun fmt -> - Format.fprintf fmt - "eager call: the statement write %a" - (PV.pp env) diff) + Format.fprintf fmt "eager: swapping statement may not write to `%a`" + (PV.pp env) diff) in List.iter check_a argsl; let modil = PV.union (f_write env fl) swl in let modir = PV.union (f_write env fr) swr in - let post = EcPhlCall.wp2_call env fpre fpost (lvl, fl, argsl) modil - - (lvr,fr,argsr) modir (es_po es) hyps in - let f_concl = f_eagerF fpre sl fl fr sr fpost in - let concl = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) (stmt []) (stmt []) post in - - FApi.xmutate1 tc `EagerCall [f_concl; concl] - -(* -------------------------------------------------------------------- *) -let check_only_global pf env s = - let sw = s_write env s in - let sr = s_read env s in - - let check_glob v _ = - if is_loc v then - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt - "swapping statement should use only global variables: %a" - (EcPrinting.pp_pv ppe) v) - in - - let check_mp _ = () in - - PV.iter check_glob check_mp sw; - PV.iter check_glob check_mp sr - -(* -------------------------------------------------------------------- *) -(* This part of the code is for automatic application of eager rules *) -(* -------------------------------------------------------------------- *) -let eager pf env s s' inv eqIs eqXs c c' eqO = - let modi = s_write env s in - let modi' = s_write env s' in - let readi = s_read env s in - - let rev st = List.rev st.s_node in - - let check_args args = - let read = List.fold_left (e_read_r env) PV.empty args in - if not (PV.indep env modi read) then raise EqObsInError in - - let check_swap_s i = - let m = is_write env [i] in - let r = is_read env [i] in - let t = - PV.indep env m modi - && PV.indep env m readi - && PV.indep env modi r - in - if not t then raise EqObsInError - in - - let remove lvl lvr eqs = - let aux eqs (pvl, tyl) (pvr, tyr) = - if (ER.EqTest.for_type env tyl tyr) - then Mpv2.remove env pvl pvr eqs - else raise EqObsInError in - - match lvl, lvr with - | LvVar xl, LvVar xr -> aux eqs xl xr - - | LvTuple ll, LvTuple lr - when List.length ll = List.length lr - -> - List.fold_left2 aux eqs ll lr - - | _, _ -> raise EqObsInError in - - let oremove lvl lvr eqs = - match lvl, lvr with - | None , None -> eqs - | Some lvl, Some lvr -> remove lvl lvr eqs - | _ , _ -> raise EqObsInError in - - let rec s_eager fhyps rsl rsr eqo = - match rsl, rsr with - | [], _ -> [], rsr, fhyps, eqo - | _ , [] -> rsl, [], fhyps, eqo - - | il::rsl', ir::rsr' -> - match (try Some (i_eager fhyps il ir eqo) with _ -> None) with - | None -> rsl, rsr, fhyps, eqo - | Some (fhyps, eqi) -> - (* we ensure that the seq rule can be apply *) - let eqi2 = i_eqobs_in_refl env ir (Mpv2.fv2 eqo) in - if not (PV.subset eqi2 (Mpv2.fv2 eqi)) then raise EqObsInError; - pf_compat pf env modi modi' eqi eqIs eqXs; - s_eager fhyps rsl' rsr' eqi - - and i_eager fhyps il ir eqo = - match il.i_node, ir.i_node with - | Sasgn (lvl, el), Sasgn (lvr, er) - | Srnd (lvl, el), Srnd (lvr, er) -> - check_swap_s il; - let eqnm = Mpv2.split_nmod env modi modi' eqo in - let eqm = Mpv2.split_mod env modi modi' eqo in - if not (Mpv2.subset eqm eqXs) then raise EqObsInError; - let eqi = Mpv2.union eqIs eqnm in - (fhyps, Mpv2.add_eqs env el er (remove lvl lvr eqi) ) - - | Scall (lvl, fl, argsl), Scall (lvr, fr, argsr) - when List.length argsl = List.length argsr - -> - check_args argsl; - let eqo = oremove lvl lvr eqo in - let modl = PV.union modi (f_write env fl) in - let modr = PV.union modi' (f_write env fr) in - let eqnm = Mpv2.split_nmod env modl modr eqo in - let outf = Mpv2.split_mod env modl modr eqo in - Mpv2.check_glob outf; - let fhyps, inf = f_eager fhyps fl fr outf in - let eqi = - List.fold_left2 - (fun eqs e1 e2 -> Mpv2.add_eqs env e1 e2 eqs) - (Mpv2.union eqnm inf) argsl argsr - in - (fhyps, eqi) - - | Sif (el, stl, sfl), Sif (er, str, sfr) -> - check_args [el]; - let r1,r2,fhyps1, eqs1 = s_eager fhyps (rev stl) (rev str) eqo in - if r1 <> [] || r2 <> [] then raise EqObsInError; - let r1,r2, fhyps2, eqs2 = s_eager fhyps1 (rev sfl) (rev sfr) eqo in - if r1 <> [] || r2 <> [] then raise EqObsInError; - let eqi = Mpv2.union eqs1 eqs2 in - let eqe = Mpv2.add_eqs env el er eqi in - (fhyps2, eqe) - - | Swhile (el, sl), Swhile (er, sr2) -> - check_args [el]; (* ensure condition (d) *) - let sl, sr = rev sl, rev sr2 in - let rec aux eqo = - let r1,r2,fhyps, eqi = s_eager fhyps sl sr eqo in - if r1 <> [] || r2 <> [] then raise EqObsInError; - if Mpv2.subset eqi eqo then fhyps, eqo - else aux (Mpv2.union eqi eqo) - in - let fhyps, eqi = aux (Mpv2.union eqIs (Mpv2.add_eqs env el er eqo)) in - (* by construction condition (a), (b) and (c) are satisfied *) - pf_compat pf env modi modi' eqi eqIs eqXs; (* ensure (e) and (f) *) - (* (h) is assumed *) - (fhyps, eqi) - - | Sassert el, Sassert er -> - check_args [el]; - let eqnm = Mpv2.split_nmod env modi modi' eqo in - let eqm = Mpv2.split_mod env modi modi' eqo in - if not (Mpv2.subset eqm eqXs) then raise EqObsInError; - let eqi = Mpv2.union eqIs eqnm in - (fhyps, Mpv2.add_eqs env el er eqi) - - | Sabstract _, Sabstract _ -> assert false (* FIXME *) - - | _, _ -> raise EqObsInError - - and f_eager fhyps fl fr out = - let fl = NormMp.norm_xfun env fl in - let fr = NormMp.norm_xfun env fr in - - let rec aux fhyps = - match fhyps with - | [] -> [fl,fr,out] - | (fl', fr', out') :: fhyps -> - if EcPath.x_equal fl fl' && EcPath.x_equal fr fr' - then (fl ,fr , Mpv2.union out out') :: fhyps - else (fl',fr', out') :: (aux fhyps) - in - aux fhyps, inv - in - - s_eager [] (rev c) (rev c') eqO - -(* -------------------------------------------------------------------- *) -let t_eager_r h inv tc = - let env, hyps, _ = FApi.tc1_eflat tc in - let _, (_, s, s', eqIs, eqXs) = pf_hSS !!tc hyps h in - - check_only_global !!tc env s; - check_only_global !!tc env s'; - - let eC, c, c' = tc1_destr_eagerS tc s s' in - let ml, mr = fst eC.es_ml, fst eC.es_mr in - let eqinv = Mpv2.of_form env inv in - let eqO = Mpv2.of_form env (es_po eC) in - let c1, c1', fhyps, eqi = eager !!tc env s s' eqinv eqIs eqXs c c' eqO in - - if c1 <> [] || c1' <> [] then - tc_error !!tc "not able to apply eager"; (* FIXME *) - - let dof (fl,fr,eqo) = - let defl = Fun.by_xpath fl env in - let defr = Fun.by_xpath fr env in - let sigl, sigr = defl.f_sig, defr.f_sig in - let eq_res = ts_inv_eqres sigl.fs_ret ml sigr.fs_ret mr in - let post = Mpv2.to_form_ts_inv eqo eq_res in - let eq_params = - ts_inv_eqparams - sigl.fs_arg sigl.fs_anames ml - sigr.fs_arg sigr.fs_anames mr in - let pre = map_ts_inv2 f_and_simpl eq_params inv in - f_eagerF pre s fl fr s' post + let post = + EcPhlCall.wp2_call env fpre fpost (lvl, fl, argsl) modil (lvr, fr, argsr) + modir (es_po es) hyps in - + let f_concl = f_eagerF fpre sl fl fr sr fpost in let concl = - f_equivS (snd eC.es_ml) (snd eC.es_mr) (es_pr eC) (stmt []) (stmt []) - (Mpv2.to_form_ts_inv eqi {ml;mr;inv=f_true}) in - - let concls = List.map dof fhyps in + f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) (stmt []) (stmt []) post + in - FApi.xmutate1 tc `EagerAuto (concl::concls) + FApi.xmutate1 tc `EagerCall [ f_concl; concl ] (* -------------------------------------------------------------------- *) -let t_eager_seq = FApi.t_low4 "eager-seq" t_eager_seq_r -let t_eager_if = FApi.t_low0 "eager-if" t_eager_if_r -let t_eager_while = FApi.t_low1 "eager-while" t_eager_while_r +let t_eager_seq = FApi.t_low3 "eager-seq" t_eager_seq_r +let t_eager_if = FApi.t_low0 "eager-if" t_eager_if_r +let t_eager_while = FApi.t_low1 "eager-while" t_eager_while_r let t_eager_fun_def = FApi.t_low0 "eager-fun-def" t_eager_fun_def_r -let t_eager_fun_abs = FApi.t_low2 "eager-fun-abs" t_eager_fun_abs_r -let t_eager_call = FApi.t_low2 "eager-call" t_eager_call_r -let t_eager = FApi.t_low2 "eager" t_eager_r +let t_eager_fun_abs = FApi.t_low1 "eager-fun-abs" t_eager_fun_abs_r +let t_eager_call = FApi.t_low2 "eager-call" t_eager_call_r (* -------------------------------------------------------------------- *) -let process_info info tc = - let hyps = FApi.tc1_hyps tc in - - match info with - | EcParsetree.LE_done h -> - (t_id tc, fst (LDecl.hyp_by_name (unloc h) hyps)) - - | EcParsetree.LE_todo (h, s1, s2, eqIs, eqXs) -> - let (ml, mlt) as mle, ((mr, mrt) as mre) = - match (FApi.tc1_goal tc).f_node with - | FeagerF {eg_ml=ml;eg_mr=mr} -> - EcMemory.abstract ml, EcMemory.abstract mr - | _ -> - let es = tc1_as_equivS tc in - es.es_ml, es.es_mr in - let hyps = LDecl.push_active_ts mle mre hyps in - let process_formula = TTC.pf_process_form !!tc hyps tbool in - let eqIs = {ml;mr;inv=process_formula eqIs} in - let eqXs = {ml;mr;inv=process_formula eqXs} in - let s1 = TTC.tc1_process_prhl_stmt tc `Left s1 in - let s2 = TTC.tc1_process_prhl_stmt tc `Right s2 in - let f = f_equivS mlt mrt eqIs s1 s2 eqXs in - let h = LDecl.fresh_id hyps (unloc h) in - (FApi.t_last (t_intros_i [h]) (t_cut f tc), h) - -(* -------------------------------------------------------------------- *) -let process_seq info (i, j) eqR tc = - let eqR = TTC.tc1_process_prhl_form tc tbool eqR in - let gs, h = process_info info tc in - let i = EcProofTyping.tc1_process_codepos1 tc (Some `Left , i) in - let j = EcProofTyping.tc1_process_codepos1 tc (Some `Right, j) in - FApi.t_last (t_eager_seq i j eqR h) gs - -(* -------------------------------------------------------------------- *) -let process_if tc = - t_eager_if tc - -(* -------------------------------------------------------------------- *) -let process_while info tc = - let gs, h = process_info info tc in - FApi.t_last (t_eager_while h) gs +let process_seq (i, j) s factor tc = + let open BatTuple.Tuple2 in + let indices = + mapn (TTC.tc1_process_codepos1 tc) ((Some `Left, i), (Some `Right, j)) + and factor = + factor + |> ( function Single p -> (p, p) | Double pp -> pp ) + |> mapn (TTC.tc1_process_prhl_form tc tbool) + and s = TTC.tc1_process_prhl_stmt tc `Left s in + + t_eager_seq indices s factor tc + +let process_if = t_eager_if + +let process_while inv tc = + (* This is performed here only to recover [e{1}] and setup + the consequence rule accordingly. *) + let es, _, w, _ = destruct_on_op `While tc in + let e, _ = destr_while w in + let e1 = ss_inv_of_expr (fst es.es_ml) e in + + let inv = TTC.tc1_process_prhl_form tc tbool inv in + (EcPhlConseq.t_equivS_conseq inv + { inv with inv = f_and inv.inv (f_not e1.inv) } + @+ [ t_trivial; t_trivial; t_eager_while inv ]) + tc -(* -------------------------------------------------------------------- *) -let process_fun_def tc = - t_eager_fun_def tc +let process_fun_def tc = t_eager_fun_def tc -(* -------------------------------------------------------------------- *) -let process_fun_abs info eqI tc = - let eg = EcLowPhlGoal.tc1_as_eagerF tc in - let ml, mr = eg.eg_ml, eg.eg_mr in - let hyps = FApi.tc1_hyps tc in - let env = LDecl.inv_memenv ml mr hyps in - let eqI = TTC.pf_process_form !!tc env tbool eqI in - let gs, h = process_info info tc in - FApi.t_last (t_eager_fun_abs {inv=eqI;ml;mr} h) gs +let process_fun_abs inv tc = + let hyps = FApi.tc1_hyps tc in + let { eg_ml = ml; eg_mr = mr } = tc1_as_eagerF tc in + let env = LDecl.inv_memenv ml mr hyps in + let inv = TTC.pf_process_formula !!tc env inv in + t_eager_fun_abs { ml; mr; inv } tc -(* -------------------------------------------------------------------- *) let process_call info tc = - let process_cut info = - match info with - | EcParsetree.CI_spec (fpre, fpost) -> - let env, hyps, _ = FApi.tc1_eflat tc in - let es = tc1_as_equivS tc in + let process_cut' fpre fpost = + let env, hyps, _ = FApi.tc1_eflat tc in + let es = tc1_as_equivS tc in - let (_,fl,_), sl = tc1_last_call tc es.es_sl in - let (_,fr,_), sr = tc1_first_call tc es.es_sr in + let (_, fl, _), sl = tc1_last_call tc es.es_sl in + let (_, fr, _), sr = tc1_first_call tc es.es_sr in - check_only_global !!tc env sl; - check_only_global !!tc env sr; + check_only_global !!tc env sl; + check_only_global !!tc env sr; - let (ml, mr) = fst es.es_ml, fst es.es_mr in - let penv, qenv = LDecl.equivF ml mr fl fr hyps in - let fpre = TTC.pf_process_form !!tc penv tbool fpre in - let fpost = TTC.pf_process_form !!tc qenv tbool fpost in - f_eagerF {ml;mr;inv=fpre} sl fl fr sr {ml;mr;inv=fpost} - - | _ -> tc_error !!tc "invalid arguments" + let ml, mr = (fst es.es_ml, fst es.es_mr) in + let penv, qenv = LDecl.equivF ml mr fl fr hyps in + let fpre = TTC.pf_process_formula !!tc penv fpre in + let fpost = TTC.pf_process_formula !!tc qenv fpost in + f_eagerF { ml; mr; inv = fpre } sl fl fr sr { ml; mr; inv = fpost } + in + let process_cut = function + | EcParsetree.CI_spec (fpre, fpost) -> process_cut' fpre fpost + | CI_inv inv -> process_cut' inv inv + | _ -> tc_error !!tc "eager: invalid call specification" in let pt, ax = - PT.tc1_process_full_closed_pterm_cut ~prcut:process_cut tc info in + PT.tc1_process_full_closed_pterm_cut ~prcut:process_cut tc info + in let eg = pf_as_eagerF !!tc ax in FApi.t_on1seq 0 (t_eager_call (eg_pr eg) (eg_po eg)) (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) tc - -(* -------------------------------------------------------------------- *) -let process_eager info inv tc = - let inv = TTC.tc1_process_prhl_form tc tbool inv in - let gs, h = process_info info tc in - FApi.t_last (t_eager h inv) gs diff --git a/src/phl/ecPhlEager.mli b/src/phl/ecPhlEager.mli index 1958df5529..6d5c2b0580 100644 --- a/src/phl/ecPhlEager.mli +++ b/src/phl/ecPhlEager.mli @@ -1,95 +1,103 @@ (* -------------------------------------------------------------------- *) +open EcAst open EcUtils open EcParsetree open EcCoreGoal.FApi open EcMatching.Position -open EcAst -(* -------------------------------------------------------------------- *) -val t_eager_seq : codepos1 -> codepos1 -> ts_inv -> EcIdent.t -> backward -val t_eager_if : backward -val t_eager_while : EcIdent.t -> backward -val t_eager_fun_def : backward -val t_eager_fun_abs : ts_inv -> EcIdent.t -> backward -val t_eager_call : ts_inv -> ts_inv -> backward +val process_seq : pcodepos1 pair -> pstmt -> pformula doption -> backward +(** Tactic [eager seq] derives the following proof: + {v + (a) S; c₁ ~ c₁'; S : P ==> R₂ + (b) S; c₂ ~ c₂'; S : R₁ ==> Q + (c) c₁' ~ c₁' : Eq ==> R₁ + (d) c₂ ~ c₂ : R₂ ==> ={Q.1} + ----------------------------------- + S; c₁; c₂ ~ c₁'; c₂'; S : P ==> Q + v} + where [R₁] and [R₂] are provided manually (and equal if a single value was + provided), as well as [S]. The predicate [={Q.1}] means equality on all free + variables bound to the first memory in [Q]. *) + +val t_eager_seq : codepos1 pair -> stmt -> ts_inv pair -> backward +(** Internal variant of [eager seq] *) + +val process_if : backward +(** Tactic [eager if] derives the following proof: + {v + (a) forall &1 &2, P => e{1} = e'{2} + (b) forall &2 b, S : P /\ e = b ==> e = b + (c) S; c₁ ~ c₁'; S : P /\ e{1} ==> Q + (d) S; c₂ ~ c₂'; S : P /\ !e{1} ==> Q + -------------------------------------------- + S; if e then c₁ else c₂ + ~ if e' then c₁' else c₂'; S : P ==> Q + v} *) + +val t_eager_if : backward +(** Internal variant of [eager if] *) + +val process_while : pformula -> backward +(** Tactic [eager while] derives the following proof: + {v + (a) I => ={e, I.1} + (b) S; c ~ c'; S : I /\ e{1} ==> I + (c) forall b &2, S : e = b ==> e = b + (d) c' ~ c' : Eq ==> I + (e) c ~ c : I ==> I + (f) S ~ S : I /\ !e{1} ==> I + -------------------------------------------------------- + S; while e do c ~ while e do c'; S : I ==> I /\ !e{1} + v} + Where the invariant [I] is manually provided. + Please note that the guard [e] is syntactically identical in both + programs. *) + +val t_eager_while : ts_inv -> backward +(** Internal variant of [eager while] *) -(* -------------------------------------------------------------------- *) -val process_seq : eager_info -> pcodepos1 pair -> pformula -> backward -val process_if : backward -val process_while : eager_info -> backward val process_fun_def : backward -val process_fun_abs : eager_info -> pformula -> backward -val process_call : call_info gppterm -> backward -val process_eager : eager_info -> pformula -> backward +(** Tactic [eager proc] derives the following proof: + {v + (0) S and S' depend only of global (typing invariant) + (a) S; f.body; result = f.res; ~ S'; f'.body; result' = f'.res + : P ==> Q{res{1} <- result, res{2} <- result'} + ---------------------------------------------------------------- + S, f ~ f', S : P ==> Q + v} *) -(* -------------------------------------------------------------------- *) -(* [eager-seq] - * (a) c1;S ~ S;c1' : P ==> ={R} - * (b) c2;S ~ S;c2' : ={R} ==> Q - * (c) c2' ~ c2' : ={R.2} ==> ={Q.2} - * (d) ={R} => ={Is} - * (e) compat S S' R Xs - * (h) S ~ S' : ={Is} ==> ={Xs} - * -------------------------------------------------- - * c1;c2;S ~ S;c1';c2' : P ==> Q - * - * where compat S S' R Xs = - * forall modS modS', ={Xs{modS,modS'}} => ={R{modS,modS'}} - * - * [eager-if] - * (a) P => e{1} = e'{2} - * (b) S;c1 ~ S';c1' : P /\ e{1} ==> Q - * (c) S;c2 ~ S';c2' : P /\ !e{1} ==> Q - * (d) forall b &2, S : P /\ e = b ==> e = b - * -------------------------------------------------- - * S;if e then c1 else c2 - * ~ if e' then c1' else c2';S' : P ==> Q - * - * [eager-while] - * - * (a) ={I} => e{1} = e{2} - * (b) S;c ~ c';S' : ={I} /\ e{1} ==> ={I} - * (c) c' ~ c' : ={I.2} ==> ={I.2} - * (d) forall b &2, S : e = b ==> e = b - * (e) ={I} => ={Is} - * (f) compat S S' I Xs - * (h) S ~ S' : ={Is} ==> ={Xs} - * -------------------------------------------------- - * S;while e do c ~ while e' do c';S' - * : ={I} ==> ={I,Xs} /\ !e{1} - * - * [eager-fun-def] - * - * (a) S and S' depend only of global - * (this should be an invariant of the typing) - * (b) S;f.body;result = f.res; ~ S';f'.body;result' = f'.res - * : P ==> Q{res{1}<- result, res{2} <- result'} - * -------------------------------------------------- - * S, f ~ f', S' : P ==> Q - * - * [eager-fun-abs] - * - * S and S' depend only of global (hould be an invariant of the typing) - * - * (a) ={I} => e{1} = e{2} - * for each oracles o o': - * o and o' do not modify (glob A) (this is implied by (f)) - * (b) S,o ~ o',S' : ={I,params} ==> ={I,res} - * (c) o'~ o' : ={I.2, o'.params} ==> ={I.2, res} - * (e) ={I} => ={Is} - * (f) compat S S' I Xs - * (h) S ~ S' : ={Is} ==> ={Xs} - * (i) glob A not in I (checked in EcPhlFun.equivF_abs_spec) - * (j) S, S' do not modify glob A - * -------------------------------------------------- - * S, A.f{o} ~ A.f(o'), S' - * : ={I,glob A,A.f.params} ==> ={I,glob A,res} - * - * Remark : ={glob A} is not required in pre condition when A.f is an initializer - * - * [eager-call] - * S,f ~ f',S' : fpre ==> fpost - * S do not write a - * -------------------------------------------------- - * S;x = f(a) ~ x' = f'(a');S' : wp_call fpre fpost post ==> post - *) +val t_eager_fun_def : backward +(** Internal variant of [eager proc] *) + +val process_call : call_info gppterm -> backward +(** Tactic [eager call] derives the following proof: + {v + (a) S, f ~ f', S : fpre ==> fpost + (b) S does not write a + ------------------------------------------------------------------ + S; x = f(a) ~ x' = f'(a'); S : wp_call fpre fpost post ==> post + v} *) + +val t_eager_call : ts_inv -> ts_inv -> backward +(** Internal variant of [eager call] *) + +val process_fun_abs : pformula -> backward +(** Tactic [eager call] (on abstract functions) derives the following proof: + {v + (0) S depends only on globals (typing invariant) + (a) I is a conjunction of same-name variable equalities + (b) glob A not in I (checked in EcPhlFun.equivF_abs_spec) + (c) S does not modify glob A + (d) S ~ S : I ==> I + for each oracles o o': + o and o' do not modify (glob A) + (e) S, o ~ o', S : I /\ ={o'.params} ==> I /\ ={res} + (f) o' ~ o' : Eq ==> I /\ ={res} + (g) o ~ o : I /\ ={o.params} ==> I /\ ={res} + -------------------------------------------------------- + S, A.f{o} ~ A.f(o'), S + : I /\ ={glob A, A.f.params} ==> I /\ ={glob A, res} + v} *) + +val t_eager_fun_abs : ts_inv -> backward +(** Internal variant of [eager call] (on abstract functions) *) diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec index c672898f6a..59fd19bc5e 100644 --- a/theories/crypto/PROM.ec +++ b/theories/crypto/PROM.ec @@ -692,8 +692,7 @@ lemma eager_D : D(RRO).distinguish, RRO.resample(); : ={glob D, FRO.m, arg} ==> ={FRO.m, glob D} /\ ={res}]. proof. -eager proc (H_: RRO.resample(); ~ RRO.resample();: ={FRO.m} ==> ={FRO.m}) - (={FRO.m}) =>//; try by sim. +eager proc (={FRO.m}) =>//; try by sim. + by apply eager_init. + by apply eager_get. + by apply eager_set. diff --git a/theories/distributions/SDist.ec b/theories/distributions/SDist.ec index ef3b2f244d..70610147a0 100644 --- a/theories/distributions/SDist.ec +++ b/theories/distributions/SDist.ec @@ -509,7 +509,7 @@ local module Gr(O : Oracle_i) = { } }. -(* TOTHINK: Can this be strenthened by dropping the requirement that +(* TOTHINK: Can this be strengthened by dropping the requirement that d1 and d2 are lossless? The current proof uses the eager tactics to swap the statement [if (Var.b) Var.x <$ Var.d;] over the call to the adversary, which only works if the distributions are lossless. *) @@ -538,12 +538,11 @@ byequiv => //. have eq_main_O1e_O1l: equiv[Game(A, O1e).main ~ Gr(O1l).main: ={arg, glob A} /\ arg{1} = d' ==> ={res}]. + proc; inline *. - seq 6 6 : (={glob Var, glob A}); 1: by auto. - eager (H : if (Var.b) Var.x <$ Var.d; ~ if (Var.b) Var.x <$ Var.d; - : ={glob Var} ==> ={glob Var} ) - : (={glob A,glob Var} ) => //; 1: by sim. -eager proc H (={glob Var}) => //; 2: by sim. - proc*; inline *; rcondf{2} 6; [ by auto | by sp; if; auto]. + seq 6 6 : (={glob Var, glob A}); 1: by auto. + eager call (: ={glob Var, glob A} ==> ={glob Var, glob A, res}) => //. + eager proc (={glob Var}) => //; try sim. + eager proc. + by inline*; rcondf{2} 6; [ by auto | by sp; if; auto]. proc. transitivity* {1} {r <@ Game(A, O1e).main(d);}. + by inline *; rcondt{2} 8; auto; call(: ={Var.x}); 1: sim; auto.