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 = { 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);}.