From 330c546b5f9684e509b12f8c8b4b971a0e9a6fe2 Mon Sep 17 00:00:00 2001 From: Lucas Tabary-Maujean Date: Tue, 17 Jun 2025 17:46:47 +0200 Subject: [PATCH 1/2] 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 | 15 +- 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 | 917 +++++++++++++------------------- src/phl/ecPhlEager.mli | 178 ++++--- theories/crypto/PROM.ec | 3 +- theories/distributions/SDist.ec | 13 +- 10 files changed, 491 insertions(+), 680 deletions(-) diff --git a/examples/PRG.ec b/examples/PRG.ec index d9573a5377..caa8ec9910 100644 --- a/examples/PRG.ec +++ b/examples/PRG.ec @@ -340,12 +340,9 @@ section. by wp; rnd; wp; rnd{2} predT; 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 proc; inline Resample.resample. + eager call (: ={glob A, glob Plog, glob F}) => //. + eager proc (={glob Plog, glob F}) => //; try by 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. sim. @@ -357,10 +354,8 @@ 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 eager proc; swap{1} 1 4; sim. - by sim. + by sim. + by eager proc; swap{1} 1 4; sim. qed. lemma P_PrgI &m: diff --git a/examples/UC/RndO.ec b/examples/UC/RndO.ec index 2450f14fbb..6c6f83c247 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 b6ba72edac..886d73db01 100644 --- a/src/ecEnv.ml +++ b/src/ecEnv.ml @@ -2351,7 +2351,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 @@ -2363,9 +2363,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 1973bef557..d15436d2e7 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -222,9 +222,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 81c38f90b7..44a8270f3c 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -2844,35 +2844,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 bc090f6932..b26f05a84f 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 @@ -774,13 +769,12 @@ type phltactic = | Pprocrewrite of side option * pcodepos * prrewrite (* 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 65d1541a67..5341eff752 100644 --- a/src/phl/ecPhlEager.ml +++ b/src/phl/ecPhlEager.ml @@ -1,279 +1,333 @@ -(* -------------------------------------------------------------------- *) -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 (fst es.es_ml) (fst es.es_mr) - with Not_found -> tc_error pf "cannot reconize a set of equalities" - in - (es, es.es_sl, es.es_sr, of_form es.es_pr, of_form es.es_po) - -(* -------------------------------------------------------------------- *) -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 +(** Builds a formula that represents equality on the list of variables [l] + between two memories [m1] and [m2] *) +let list_eq_to_form m1 m2 (l, l_glob) = + let to_form m = List.map (fun (pv, ty) -> f_pvar pv ty m) in + let to_form_glob m = List.map (fun x -> f_glob (EcPath.mget_ident x) m) in + f_eqs + (to_form m1 l @ to_form_glob m1 l_glob) + (to_form m2 l @ to_form_glob m2 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{m1} \/ b{m3} /\ c{m1})], (with [m1] the first + argument, [m2] the second and [m3] another memory, distinct from [m1]) then + this function returns [(a{m1} = a{m2} /\ c{m1} = c{m2})]. The result of this + operation is sometimes denoted [={q.m1}]. *) +let eq_on_sided_form env m1 m2 q = + PV.fv env m1 q |> PV.elements |> list_eq_to_form m1 m2 + +(** Returns a formula that describes equality on all variables from both + memories in predicate [q], 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 m1 m2 q c = + s_read env c + |> PV.union (PV.fv env m1 q) + |> PV.union (PV.fv env m2 q) + |> PV.elements |> list_eq_to_form m1 m2 + +(** 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 z_eq_s = List.all2 i_equal z s.s_node + and z'_eq_s = List.all2 i_equal z' s.s_node 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 eqR = Mpv2.to_form mleft mright eqR f_true in - let eqIs = Mpv2.to_form mleft mright eqIs f_true in - tc_error_lazy pf (fun fmt -> - let ppe = EcPrinting.PPEnv.ofenv env in - Format.fprintf fmt "%a should be include in %a" - (EcPrinting.pp_form ppe) eqIs (EcPrinting.pp_form ppe) eqR) - 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 (fst eC.es_ml) (fst eC.es_mr) 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) eC.es_po) 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 (fst eC.es_ml) (fst eC.es_mr) eq f_true in - - let a = f_equivS_r { eC with - es_sl = stmt (s.s_node@c1); - es_sr = stmt (c1'@s'.s_node); - es_po = eqR; - } - and b = f_equivS_r { eC with - es_pr = eqR; - es_sl = stmt (s.s_node@c2); - es_sr = stmt (c2'@s'.s_node); - } - and c = f_equivS_r { eC with - es_ml = (fst eC.es_ml, snd eC.es_mr); - es_pr = to_form (Mpv2.eq_fv2 seqR); - es_sl = stmt c2'; - es_sr = stmt c2'; - es_po = to_form eqO2; - } - +(* 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 m1 = fst eC.es_ml + and m2 = fst eC.es_mr + and c1, c2 = s_split env i c + and c1', c2' = s_split env j c' in + let eqMem1 = eq_on_form_and_stmt env m1 m2 r1 (stmt c1') + and eqQ1 = eq_on_sided_form env m1 m2 eC.es_po in + + let a = + f_equivS_r + { + eC with + es_sl = stmt (s.s_node @ c1); + es_sr = stmt (c1' @ s.s_node); + es_po = r2; + } + and b = + f_equivS_r + { + eC with + es_pr = r1; + es_sl = stmt (s.s_node @ c2); + es_sr = stmt (c2' @ s.s_node); + } + and c = + f_equivS_r + { + eC with + es_ml = (fst eC.es_ml, snd eC.es_mr); + es_pr = eqMem1; + es_sl = stmt c1'; + es_sr = stmt c1'; + es_po = r1; + } + and d = + f_equivS_r + { + eC with + es_mr = (fst eC.es_mr, snd eC.es_ml); + es_pr = r2; + es_sl = stmt c2; + es_sr = stmt c2; + es_po = eqQ1; + } in - - FApi.t_first - (t_apply_hyp h) - (FApi.xmutate1 tc `EagerSeq [tH; a; b; c]) + FApi.xmutate1 tc `EagerSeq [ a; b; c; d ] (* -------------------------------------------------------------------- *) let t_eager_if_r tc = - let hyps = FApi.tc1_hyps tc in - let es = tc1_as_equivS tc 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 hyps = FApi.tc1_hyps tc and 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 = form_of_expr (fst es.es_ml) e in let fer = form_of_expr (fst es.es_mr) e' in - let fe = form_of_expr mhr e in + let fe = form_of_expr mhr e in - let m2 = as_seq1 (LDecl.fresh_ids hyps ["&m2"]) in + let m2 = as_seq1 (LDecl.fresh_ids hyps [ "&m2" ]) in let aT = f_forall - [(mleft, GTmem (snd es.es_ml)); (mright, GTmem (snd es.es_mr))] - (f_imp es.es_pr (f_eq fel fer)) in + [ (mleft, GTmem (snd es.es_ml)); (mright, GTmem (snd es.es_mr)) ] + (f_imp es.es_pr (f_eq fel fer)) + in let bT = - let b = EcIdent.create "b1" in - let eqb = f_eq fe (f_local b tbool) in - let sub = Fsubst.f_subst_id in - let sub = Fsubst.f_bind_mem sub mleft mhr in - let sub = Fsubst.f_bind_mem sub mright m2 in - let p = Fsubst.f_subst sub es.es_pr in + let bind m1 m2 s = Fsubst.f_bind_mem s m1 m2 and b = EcIdent.create "b1" in + let eqb = f_eq fe (f_local b tbool) + and p = + Fsubst.f_subst_id |> bind mleft mhr |> bind mright m2 |> fun s -> + Fsubst.f_subst s es.es_pr + in f_forall - [(m2, GTmem (snd es.es_mr)); (b, GTty tbool)] - (f_hoareS (mhr, snd es.es_ml) (f_and p eqb) s eqb) in + [ (m2, GTmem (snd es.es_mr)); (b, GTty tbool) ] + (f_hoareS (mhr, snd es.es_ml) (f_and p eqb) s eqb) + in let cT = let pre = f_and es.es_pr (f_eq fel 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 es.es_ml es.es_mr pre st st' es.es_po in + let st = stmt (s.s_node @ c1.s_node) in + let st' = stmt (c1'.s_node @ s.s_node) in + f_equivS es.es_ml es.es_mr pre st st' es.es_po + in let dT = let pre = f_and es.es_pr (f_eq fel 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 es.es_ml es.es_mr pre st st' es.es_po in + let st = stmt (s.s_node @ c2.s_node) in + let st' = stmt (c2'.s_node @ s.s_node) in + f_equivS es.es_ml es.es_mr pre st st' es.es_po + 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 t_eager_while_r i tc = let env, hyps, _ = 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 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 + let m1 = fst es.es_ml and m2 = fst es.es_mr in + let eqMem1 = eq_on_form_and_stmt env m1 m2 i c' + and eqI = eq_on_sided_form env m1 m2 i 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 e1 = form_of_expr (fst es.es_ml) e in + let e2 = form_of_expr (fst es.es_mr) e' in + let fe = form_of_expr mhr e in - let to_form eq = Mpv2.to_form (fst eC.es_ml) (fst eC.es_mr) eq f_true in - - let eqI = eC.es_pr in - let seqI = - try - Mpv2.of_form env (fst eC.es_ml) (fst eC.es_mr) 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) - in - let eqI2 = to_form (Mpv2.eq_fv2 seqI) in - let e1 = form_of_expr (fst eC.es_ml) e in - let e2 = form_of_expr (fst eC.es_mr) e' in - let post = Mpv2.to_form (fst eC.es_ml) (fst eC.es_mr) (Mpv2.union seqI eqXs) (f_not e1) in - - (* check (e) and (f) *) - pf_compat !!tc env (s_write env s) (s_write env s') seqI eqIs eqXs; + let m2 = as_seq1 (LDecl.fresh_ids hyps [ "&m2" ]) in let aT = f_forall - [mleft,GTmem (snd eC.es_ml); mright, GTmem (snd eC.es_mr)] - (f_imp eqI (f_eq e1 e2)) - - and bT = f_equivS_r { eC with - es_pr = f_and_simpl eqI e1; - es_sl = stmt (s.s_node@c.s_node); - es_sr = stmt (c'.s_node@s'.s_node); - es_po = eqI; - } - - and cT = f_equivS_r { eC with - es_ml = (fst eC.es_ml, snd eC.es_mr); - es_pr = eqI2; - es_sl = c'; - es_sr = c'; - es_po = eqI2; - } - - in - - let tsolve tc = - FApi.t_first - (t_apply_hyp h) - (FApi.xmutate1 tc `EagerWhile [tH; aT; bT; cT]) + [ (mleft, GTmem (snd es.es_ml)); (mright, GTmem (snd es.es_mr)) ] + (f_imp i (f_eq e1 e2)) + and bT = + f_equivS_r + { + es with + es_pr = f_and_simpl i e1; + es_sl = stmt (s.s_node @ c.s_node); + es_sr = stmt (c'.s_node @ s.s_node); + es_po = i; + } + and cT = + let bind m1 m2 s = Fsubst.f_bind_mem s m1 m2 and b = EcIdent.create "b1" in + let eqb = f_eq fe (f_local b tbool) + and p = + Fsubst.f_subst_id |> bind mleft mhr |> bind mright m2 |> fun s -> + Fsubst.f_subst s es.es_pr + in + f_forall + [ (m2, GTmem (snd es.es_mr)); (b, GTty tbool) ] + (f_hoareS (mhr, snd es.es_ml) (f_and p eqb) s eqb) + and dT = + f_equivS_r { es with es_pr = eqMem1; es_sl = c'; es_sr = c'; es_po = i } + and eT = f_equivS_r { es with es_pr = i; es_sl = c; es_sr = c; es_po = eqI } + and fT = + f_equivS_r + { es with es_pr = f_and i (f_not e1); es_sl = s; es_sr = s; es_po = 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 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 fl fr env in + let memenvl, (fsigl, fdefl), memenvr, (fsigr, fdefr), env = + Fun.equivS fl fr env + in let extend mem fdef = match fdef.f_ret with - | None -> 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), + 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 s in let s = PVM.add env pv_res mr er s in @@ -283,54 +337,61 @@ let t_eager_fun_def_r tc = let s = EcPhlFun.subst_pre env fsigr mr s in let pre = PVM.subst env s eg.eg_pr in - let cond = f_equivS_r { - es_ml = meml; - es_mr = memr; - es_sl = s_seq eg.eg_sl sfl; - es_sr = s_seq sfr eg.eg_sr; - es_pr = pre; - es_po = post; - } in + let cond = + f_equivS_r + { + es_ml = meml; + es_mr = memr; + es_sl = s_seq eg.eg_sl sfl; + es_sr = s_seq sfr eg.eg_sr; + es_pr = pre; + es_po = 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 + and mleft' = EcMemory.abstract mleft + and mright' = EcMemory.abstract mright 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 mleft mright i) 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 mleft mright - (Mpv2.eq_refl (PV.fv env mright f)) - f_true - in - f_eagerF ef.ef_pr s ef.ef_fl ef.ef_fr s' ef.ef_po - :: f_equivF (torefl ef.ef_pr) ef.ef_fr ef.ef_fr (torefl ef.ef_po) - :: sg + f_eagerF ef.ef_pr s ef.ef_fl ef.ef_fr s ef.ef_po in - let sg = List.fold_right do1 sg [] in - let seqI = Mpv2.of_form env mleft mright eqI in + let do_f og = + let ef = destr_equivF og in + let eqMem = eq_on_fun env mleft mright ef.ef_fr in + f_equivF (f_and eqMem ef.ef_pr) ef.ef_fl ef.ef_fl ef.ef_po + in - (* check (e) and (f)*) - pf_compat !!tc env (s_write env s) (s_write env s') seqI eqIs eqXs; + let sg_e = List.map do_e sg_e and sg_f = List.map do_f sg_f 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)) - 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 mleft' mright' 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) @@ -339,21 +400,20 @@ let t_eager_call_r fpre fpost tc = let env, hyps, _ = FApi.tc1_eflat tc in let es = tc1_as_equivS tc 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; @@ -362,318 +422,89 @@ let t_eager_call_r fpre fpost tc = let mr = EcMemory.memory es.es_mr in 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 ml mr es.es_po hyps in - let f_concl = f_eagerF fpre sl fl fr sr fpost in - let concl = f_equivS_r { es with es_sl = stmt []; es_sr = stmt []; es_po = 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 + let post = + EcPhlCall.wp2_call env fpre fpost (lvl, fl, argsl) modil (lvr, fr, argsr) + modir ml mr es.es_po hyps 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 eqinv = Mpv2.of_form env mleft mright inv in - let eqO = Mpv2.of_form env mleft mright eC.es_po 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 = f_eqres sigl.fs_ret mleft sigr.fs_ret mright in - let post = Mpv2.to_form mleft mright eqo eq_res in - let eq_params = - f_eqparams - sigl.fs_arg sigl.fs_anames mleft - sigr.fs_arg sigr.fs_anames mright in - let pre = f_and_simpl eq_params inv in - f_eagerF pre s fl fr s' post - in - + let f_concl = f_eagerF fpre sl fl fr sr fpost in let concl = - f_equivS_r { eC with - es_sl = stmt []; es_sr = stmt []; - es_po = Mpv2.to_form mleft mright eqi f_true; - } + f_equivS_r { es with es_sl = stmt []; es_sr = stmt []; es_po = post } in - let concls = List.map dof fhyps 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,mr = - match (FApi.tc1_goal tc).f_node with - | FeagerF _ -> - EcEnv.Fun.inv_memory `Left, EcEnv.Fun.inv_memory `Right - | _ -> - let es = tc1_as_equivS tc in - es.es_ml, es.es_mr in - let hyps = LDecl.push_all [ml; mr] hyps in - let process_formula = TTC.pf_process_form !!tc hyps tbool in - let eqIs = process_formula eqIs in - let eqXs = process_formula eqXs in - let s1 = TTC.tc1_process_stmt tc (snd ml) s1 in - let s2 = TTC.tc1_process_stmt tc (snd mr) s2 in - let f = f_equivS ml mr 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_seq (i, j) s factor tc = + let open BatTuple.Tuple2 in + let mem_ty = FApi.tc1_goal tc |> destr_equivS |> fun x -> x.es_mr |> snd 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_stmt tc mem_ty 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 = form_of_expr (fst es.es_ml) e in + + let inv = TTC.tc1_process_prhl_form tc tbool inv in + (EcPhlConseq.t_equivS_conseq inv (f_and inv (f_not e1)) + @+ [ t_trivial; t_trivial; t_eager_while inv ]) + tc -(* -------------------------------------------------------------------- *) -let process_while info tc = - let gs, h = process_info info tc in - FApi.t_last (t_eager_while h) gs +let process_fun_def tc = t_eager_fun_def tc -(* -------------------------------------------------------------------- *) -let process_fun_def tc = - t_eager_fun_def tc +let process_fun_abs i tc = + let mleft, mright = (Fun.inv_memory `Left, Fun.inv_memory `Right) in + let hyps = LDecl.push_all [ mleft; mright ] (FApi.tc1_hyps tc) in + let i = TTC.pf_process_formula !!tc hyps i in + t_eager_fun_abs i tc -(* -------------------------------------------------------------------- *) -let process_fun_abs info eqI tc = - let hyps = FApi.tc1_hyps tc in - let env = LDecl.inv_memenv 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 eqI h) gs - -(* -------------------------------------------------------------------- *) 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 penv, qenv = LDecl.equivF 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 fpre sl fl fr sr fpost - - | _ -> tc_error !!tc "invalid arguments" + let penv, qenv = LDecl.equivF 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 fpre sl fl fr sr 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.eg_pr eg.eg_po) (EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt) tc - -(* -------------------------------------------------------------------- *) -let process_eager info inv tc = - let hyps = FApi.tc1_hyps tc in - let penv = LDecl.inv_memenv hyps in - let inv = TTC.pf_process_formula !!tc penv 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 b105deae2c..b0d5cc9489 100644 --- a/src/phl/ecPhlEager.mli +++ b/src/phl/ecPhlEager.mli @@ -5,91 +5,99 @@ open EcFol open EcCoreGoal.FApi open EcMatching.Position -(* -------------------------------------------------------------------- *) -val t_eager_seq : codepos1 -> codepos1 -> form -> 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 : EcFol.form -> EcIdent.t -> backward -val t_eager_call : form -> form -> 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 -> EcAst.stmt -> form pair -> backward +(** Internal variant of [eager seq] *) + +val process_if : backward +(** Tactic [eager if] derives the following proof: + {v + (a) P => e{1} = e'{2} + (b) S; c₁ ~ c₁'; S : P /\ e{1} ==> Q + (c) S; c₂ ~ c₂'; S : P /\ !e{1} ==> Q + (d) forall b &2, S : P /\ e = b ==> e = b + -------------------------------------------- + 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{1} = e'{2} + (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.1} + (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. *) + +val t_eager_while : form -> 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 : form -> form -> 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 : form -> backward +(** Internal variant of [eager call] (on abstract functions) *) diff --git a/theories/crypto/PROM.ec b/theories/crypto/PROM.ec index c2d76c7bd8..4b0577505e 100644 --- a/theories/crypto/PROM.ec +++ b/theories/crypto/PROM.ec @@ -682,8 +682,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 b3cbece743..4f0c6ce101 100644 --- a/theories/distributions/SDist.ec +++ b/theories/distributions/SDist.ec @@ -504,7 +504,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. *) @@ -533,12 +533,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. print Game. transitivity* {1} {r <@ Game(A, O1e).main(d);}. From c3c25b6ef69da75e136a97324719d4064244123c Mon Sep 17 00:00:00 2001 From: Lucas Tabary-Maujean Date: Tue, 1 Jul 2025 14:45:35 +0200 Subject: [PATCH 2/2] fix(examples): missing hints for smt-proved goal --- examples/MEE-CBC/RCPA_CMA.ec | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/MEE-CBC/RCPA_CMA.ec b/examples/MEE-CBC/RCPA_CMA.ec index 1660746704..3c1f427c38 100644 --- a/examples/MEE-CBC/RCPA_CMA.ec +++ b/examples/MEE-CBC/RCPA_CMA.ec @@ -336,7 +336,7 @@ theory EtM. type leaks <- leaks, op leak <- leak, op dC (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>) - proof * by smt. + proof * by smt(dC_ll dprod_ll dunit_ll). (** The black-box construction is as follows **) module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {