From 12af606772a9093ee2feb443da13277a7868e6ed Mon Sep 17 00:00:00 2001 From: Cameron Low Date: Fri, 15 Dec 2023 10:45:02 +0000 Subject: [PATCH] New tactic: `outline` (#473) The main idea is to provide an inverse to inline when proving an equiv. Currently, it supports basic procedure unification that requires manual selection of the program slice to unify with, as well as, requiring near exact matches on program structure. An optional return value can be supplied for situations where the return expression is just a program variable and needs to be renamed/deconstructed. There is also support for statement outlining although, this is more of a transitivity * with program slicing so may require change. Syntax and variants: - Procedure outlining: outline {m} [s - e] lv? <@ M.foo - Statement outlining: outline {m} [s - e] { s1; s2; ... } with - m: 1 or 2 - s,e: code position - M.foo: path to procedure - lv: a left-value when `s = e`, one can use `[s]` instead of `[s-s]` For example usage see: tests/outline.ec --- src/ecCoreModules.ml | 8 ++ src/ecCoreModules.mli | 1 + src/ecHiTacticals.ml | 1 + src/ecLexer.mll | 1 + src/ecParser.mly | 13 ++ src/ecParsetree.ml | 13 ++ src/ecUnifyProc.ml | 115 +++++++++++++++ src/ecUnifyProc.mli | 43 ++++++ src/phl/ecPhlOutline.ml | 298 +++++++++++++++++++++++++++++++++++++++ src/phl/ecPhlOutline.mli | 9 ++ tests/outline.ec | 130 +++++++++++++++++ 11 files changed, 632 insertions(+) create mode 100644 src/ecUnifyProc.ml create mode 100644 src/ecUnifyProc.mli create mode 100644 src/phl/ecPhlOutline.ml create mode 100644 src/phl/ecPhlOutline.mli create mode 100644 tests/outline.ec diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml index 285569cdda..1ecb5ed356 100644 --- a/src/ecCoreModules.ml +++ b/src/ecCoreModules.ml @@ -43,6 +43,14 @@ let name_of_lv lv = | LvTuple pvs -> String.concat "_" (List.map (EcTypes.name_of_pvar |- fst) pvs) +let lv_of_expr e = + match e.e_node with + | Evar pv -> + LvVar (pv, e_ty e) + | Etuple pvs -> + LvTuple (List.map (fun e -> EcTypes.destr_var e, e_ty e) pvs) + | _ -> failwith "failed to construct lv from expr" + (* -------------------------------------------------------------------- *) type instr = EcAst.instr diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli index 71a8eec3b7..961a482c16 100644 --- a/src/ecCoreModules.mli +++ b/src/ecCoreModules.mli @@ -12,6 +12,7 @@ val ty_of_lv : lvalue -> EcTypes.ty val lv_of_list : (prog_var * ty) list -> lvalue option val lv_to_list : lvalue -> prog_var list val name_of_lv : lvalue -> string +val lv_of_expr : expr -> lvalue (* --------------------------------------------------------------------- *) type instr = EcAst.instr diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 6272daaa2e..d50432deba 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -189,6 +189,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pcallconcave info -> EcPhlCall.process_call_concave info | Pswap sw -> EcPhlSwap.process_swap sw | Pinline info -> EcPhlInline.process_inline info + | Poutline info -> EcPhlOutline.process_outline info | Pinterleave info -> EcPhlSwap.process_interleave info | Pcfold info -> EcPhlCodeTx.process_cfold info | Pkill info -> EcPhlCodeTx.process_kill info diff --git a/src/ecLexer.mll b/src/ecLexer.mll index 82bb7ea451..e5917ee403 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -154,6 +154,7 @@ "conseq" , CONSEQ ; (* KW: tactic *) "exfalso" , EXFALSO ; (* KW: tactic *) "inline" , INLINE ; (* KW: tactic *) + "outline" , OUTLINE ; (* KW: tactic *) "interleave" , INTERLEAVE ; (* KW: tactic *) "alias" , ALIAS ; (* KW: tactic *) "weakmem" , WEAKMEM ; (* KW: tactic *) diff --git a/src/ecParser.mly b/src/ecParser.mly index 80893a255c..dfac80454d 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -512,6 +512,7 @@ %token NOTATION %token OF %token OP +%token OUTLINE %token PCENT %token PHOARE %token PIPE @@ -3129,6 +3130,10 @@ interleave_info: | s=side? c1=interleavepos c2=interleavepos c3=interleavepos* k=word { (s, c1, c2 :: c3, k) } +%inline outline_kind: +| s=brace(stmt) { OKstmt(s) } +| r=sexpr? LEAT f=loc(fident) { OKproc(f, r) } + phltactic: | PROC { Pfun `Def } @@ -3219,6 +3224,14 @@ phltactic: | INLINE s=side? u=inlineopt? p=codepos { Pinline (`CodePos (s, u, p)) } +| OUTLINE s=side LBRACKET st=codepos1 e=option(MINUS e=codepos1 {e}) RBRACKET k=outline_kind + { Poutline { + outline_side = s; + outline_start = st; + outline_end = odfl st e; + outline_kind = k } + } + | KILL s=side? o=codepos { Pkill (s, o, Some 1) } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 5c754039c4..02e6bf7a3a 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -670,6 +670,18 @@ type inline_info = [ (* | `All of oside * inlineopt *) ] +(* -------------------------------------------------------------------- *) +type outline_kind = + | OKstmt of pstmt + | OKproc of pgamepath * pexpr option + +type outline_info = { + outline_side: side; + outline_start: codepos1; + outline_end: codepos1; + outline_kind: outline_kind; +} + (* -------------------------------------------------------------------- *) type fel_info = { pfel_cntr : pformula; @@ -731,6 +743,7 @@ type phltactic = | Pswap of ((oside * swap_kind) located list) | Pcfold of (oside * codepos * int option) | Pinline of inline_info + | Poutline of outline_info | Pinterleave of interleave_info located | Pkill of (oside * codepos * int option) | Prnd of oside * semrndpos option * rnd_tac_info_f diff --git a/src/ecUnifyProc.ml b/src/ecUnifyProc.ml new file mode 100644 index 0000000000..836aabc656 --- /dev/null +++ b/src/ecUnifyProc.ml @@ -0,0 +1,115 @@ +open EcAst +open EcTypes +open EcModules +open EcSymbols + +(*---------------------------------------------------------------------------------------*) +type u_error = + | UE_InvalidRetInstr + | UE_UnexpectedReturn + | UE_ExprNotInLockstep of expr * expr + | UE_InstrNotInLockstep of instr * instr + | UE_DifferentProgramLengths of stmt * stmt + +exception UnificationError of u_error + +(*---------------------------------------------------------------------------------------*) +type u_value = + | Empty + | Fixed of expr + +type umap = u_value Msym.t + +(*---------------------------------------------------------------------------------------*) +let rec unify_exprs umap e1 e2 = + match e1.e_node, e2.e_node with + | Eint _, Eint _ -> umap + | Elocal _, Elocal _ -> umap + | Evar pv, e2n -> + let var = symbol_of_pv pv in + + (* Only update a value if it hasn't been fixed previously *) + let update value = + match value with + | None -> + begin + match e2n with + | Evar _ -> None + | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2))) + end + | Some Empty -> Some (Fixed e2) + | _ -> value + in + + Msym.change update var umap + | Eop _, Eop _ -> umap + | Eapp (f1, a1), Eapp (f2, a2) -> + let umap = unify_exprs umap f1 f2 in + List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine a1 a2) + | Equant (_, _, e1), Equant (_, _, e2) -> + unify_exprs umap e1 e2 + | Elet (_, e1, u1), Elet (_, e2, u2) -> + let umap = unify_exprs umap e1 e2 in + unify_exprs umap u1 u2 + | Etuple t1, Etuple t2 -> + List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine t1 t2) + | Eif (c1, t1, f1), Eif (c2, t2, f2) -> + let umap = unify_exprs umap c1 c2 in + let umap = unify_exprs umap t1 t2 in + unify_exprs umap f1 f2 + | Ematch (c1, p1, _), Ematch (c2, p2, _) -> + let umap = unify_exprs umap c1 c2 in + List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine p1 p2) + | Eproj (e1, _), Eproj (e2, _) -> + unify_exprs umap e1 e2 + | _ -> raise (UnificationError (UE_ExprNotInLockstep (e1, e2))) + +(*---------------------------------------------------------------------------------------*) +let rec unify_instrs umap i1 i2 = + match i1.i_node, i2.i_node with + | Sasgn(_, e1), Sasgn(_, e2) + | Srnd(_, e1), Srnd(_, e2) -> + unify_exprs umap e1 e2 + | Scall(_, _, args1), Scall(_, _, args2) -> + List.fold_left (fun umap (e1, e2) -> unify_exprs umap e1 e2) umap (List.combine args1 args2) + | Sif(e1, st1, sf1), Sif(e2, st2, sf2) -> + let umap = unify_exprs umap e1 e2 in + let umap = unify_stmts umap st1 st2 in + unify_stmts umap sf1 sf2 + | Swhile(e1, s1), Swhile(e2, s2) -> + let umap = unify_exprs umap e1 e2 in + unify_stmts umap s1 s2 + | Smatch(e1, bs1), Smatch(e2, bs2) -> + let umap = unify_exprs umap e1 e2 in + List.fold_left (fun umap (b1, b2) -> unify_stmts umap (snd b1) (snd b2)) umap (List.combine bs1 bs2) + | Sassert e1, Sassert e2 -> + unify_exprs umap e1 e2 + | Sabstract _, Sabstract _ -> umap + | _ -> raise (UnificationError (UE_InstrNotInLockstep (i1, i2))); + +and unify_stmts umap s1 s2 = + let s1n, s2n = s1.s_node, s2.s_node in + if List.length s1n <> List.length s2n then + raise (UnificationError (UE_DifferentProgramLengths (s1, s2))); + List.fold_left (fun umap (i1, i2) -> unify_instrs umap i1 i2) umap (List.combine s1n s2n) + +(*---------------------------------------------------------------------------------------*) +(* Given a function definition attempt to unify its body with the statements `sb` + and if a return statement is given, also unify it's expression. *) +let unify_func umap fdef sb sr = + (* Unify the body *) + let umap = unify_stmts umap fdef.f_body sb in + + (* Unify the return stmt (if it exists) and retrieve its lv *) + match sr with + | Some i -> begin + (* Check that there is a return expression to unify with *) + if fdef.f_ret = None then + raise (UnificationError UE_UnexpectedReturn); + + (* Only unify with assignment instructions *) + match i.i_node with + | Sasgn (lv, e) -> Some lv, unify_exprs umap (Option.get fdef.f_ret) e + | _ -> raise (UnificationError UE_InvalidRetInstr) + end + | _ -> None, umap diff --git a/src/ecUnifyProc.mli b/src/ecUnifyProc.mli new file mode 100644 index 0000000000..38b60a2754 --- /dev/null +++ b/src/ecUnifyProc.mli @@ -0,0 +1,43 @@ +open EcTypes +open EcModules +open EcSymbols + +(*---------------------------------------------------------------------------------------*) +(* `Unification` of procedures *) +(* + Given: r <@ foo(a1: t1, a2: t2, ...); and s1; s2; ...; sr. + Attempt to find values for a1, a2, ... such that, the body of `foo` with a1, a2, ... + replaced will exactly match s1; s2; ..., and that `r <- res` match sr. + Where `res` is the return expression of `foo`. + + Currently, this is done by traversing the respective ASTs and when a relevant + program variable is encountered on the lhs, use the rhs expression. + + FIXME: This is incredibly basic and should be iterated on with a more advanced + procedure unification algorithm. + *) + +(*---------------------------------------------------------------------------------------*) +type u_error = + | UE_InvalidRetInstr + | UE_UnexpectedReturn + | UE_ExprNotInLockstep of expr * expr + | UE_InstrNotInLockstep of instr * instr + | UE_DifferentProgramLengths of stmt * stmt + +exception UnificationError of u_error + +(*---------------------------------------------------------------------------------------*) +type u_value = + | Empty + | Fixed of expr + +type umap = u_value Msym.t + +(*---------------------------------------------------------------------------------------*) +(* The following functions attempt to unify unknown program variables + in the lhs with expressions from the rhs *) +val unify_exprs : umap -> expr -> expr -> umap +val unify_instrs : umap -> instr -> instr -> umap +val unify_stmts : umap -> stmt -> stmt -> umap +val unify_func : umap -> function_def -> stmt -> instr option -> lvalue option * umap diff --git a/src/phl/ecPhlOutline.ml b/src/phl/ecPhlOutline.ml new file mode 100644 index 0000000000..3f9f6388ef --- /dev/null +++ b/src/phl/ecPhlOutline.ml @@ -0,0 +1,298 @@ +open EcParsetree +open EcFol +open EcUtils +open EcModules +open EcTypes +open EcSymbols +open EcUnifyProc + +open EcCoreGoal +open EcCoreGoal.FApi +open EcLowGoal +open EcLowPhlGoal + +(*---------------------------------------------------------------------------------------*) +(* + Transitivity star with (ideally) lossless pre-conditions over the intermediate + programs, and automatic discharging of the first two goals. +*) +(* FIXME: Move to ecPhlTrans *) + +let t_equivS_trans_eq side s tc = + let env = tc1_env tc in + let es = tc1_as_equivS tc in + let c,m = match side with `Left -> es.es_sl, es.es_ml | `Right -> es.es_sr, es.es_mr in + + let mem_pre = split_sided (EcMemory.memory m) es.es_pr in + let fv_pr = EcPV.PV.fv env (EcMemory.memory m) es.es_pr in + let fv_po = EcPV.PV.fv env (fst m) es.es_po in + let fv_r = EcPV.s_read env c in + let mk_eqs fv = + let vfv, gfv = EcPV.PV.elements fv in + let veq = List.map (fun (x,ty) -> f_eq (f_pvar x ty mleft) (f_pvar x ty mright)) vfv in + let geq = List.map (fun mp -> f_eqglob mp mleft mp mright) gfv in + f_ands (veq @ geq) in + let pre = mk_eqs (EcPV.PV.union (EcPV.PV.union fv_pr fv_po) fv_r) in + let pre = f_and pre (odfl f_true mem_pre) in + let post = mk_eqs fv_po in + let c1, c2 = + if side = `Left then (pre, post), (es.es_pr, es.es_po) + else (es.es_pr, es.es_po), (pre, post) + in + + let exists_subtac (tc : tcenv1) = + (* Ideally these are guaranteed fresh *) + let pl = EcIdent.create "&p__1" in + let pr = EcIdent.create "&p__2" in + let h = EcIdent.create "__" in + let tc = t_intros_i_1 [pl; pr; h] tc in + let goal = tc1_goal tc in + + let p = match side with | `Left -> pl | `Right -> pr in + let b = match side with | `Left -> true | `Right -> false in + + let handle_exists () = + (* Pairing up the correct variables for the exists intro *) + let vs, fm = EcFol.destr_exists goal in + let eqs_pre, _ = + let l, r = EcFol.destr_and fm in + if b then l, r else r, l + in + let eqs, _ = destr_and eqs_pre in + let eqs = destr_ands ~deep:false eqs in + let doit eq = + let l, r = destr_eq eq in + let l, r = if b then r, l else l, r in + let v = EcFol.destr_local l in + v, r + in + let eqs = List.map doit eqs in + let exvs = + List.map + (fun (id, _) -> + let v = List.assoc id eqs in + Fsubst.f_subst_mem (EcMemory.memory m) p v) + vs + in + + as_tcenv1 (t_exists_intro_s (List.map paformula exvs) tc) + in + + let tc = + if EcFol.is_exists goal then + handle_exists () + else + tc + in + + t_seq + (t_generalize_hyp ?clear:(Some `Yes) h) + EcHiGoal.process_done + tc + in + + let tc = t_seqsub + (EcPhlTrans.t_equivS_trans (EcMemory.memtype m, s) c1 c2) + [exists_subtac; EcHiGoal.process_done; t_id; t_id] + tc + in + tc + +(*---------------------------------------------------------------------------------------*) +(* + This is the improved transitivity star from above but allows for a range of code + positions to select the program slice that is changing. The prefix and suffix are + extracted and copied across to build the new program. +*) +(* FIXME: Maybe move to ecPhlTrans as well *) + +let t_outline_stmt side start_pos end_pos s tc = + let goal = tc1_as_equivS tc in + + (* Check which memory/program we are outlining *) + let code = match side with + | `Left -> goal.es_sl + | `Right -> goal.es_sr + in + + (* Extract the program prefix and suffix *) + let rest, code_suff = s_split end_pos code in + let code_pref, _, _ = s_split_i start_pos (stmt rest) in + + let new_prog = s_seq (s_seq (stmt code_pref) s) (stmt code_suff) in + let tc = t_equivS_trans_eq side new_prog tc in + + (* The middle goal, showing equivalence with the replaced code, ideally solves. *) + let tp = match side with | `Left -> 1 | `Right -> 2 in + let p = EcHiGoal.process_tfocus tc (Some [Some tp, Some tp], None) in + let tc = + t_onselect + p + (t_try ( + t_seqs [ + EcPhlInline.process_inline (`ByName (None, None, ([], None))); + EcPhlEqobs.process_eqobs_in none {sim_pos = none; sim_hint = ([], none); sim_eqs = none}; + EcPhlAuto.t_auto; + EcHiGoal.process_done; + ])) + tc + in + tc + +(*---------------------------------------------------------------------------------------*) +(* The main tactic *) + +type out_error = + | OE_InvalidFunc + | OE_UnnecessaryReturn + | OE_UnificationFailure of EcSymbols.symbol + +exception OutlineError of out_error + +(* + `outline` - replace a program slice with a procedure call. + + Arguments, + side: selects the program (left or right) that will outlined. + start_pos, end_pos: selects the particular slice of the program to outline. + fname: path of the function that we are using to outline. + res_lv: optional left-value for the result. + when None, assume the entire slice contains the body and return. + otherwise, assume entire slice contains just the body. +*) +let t_outline_proc side start_pos end_pos fname res_lv tc = + let env = tc1_env tc in + let goal = tc1_as_equivS tc in + + (* Extract the function args, body, and return expression *) + let func = EcEnv.Fun.by_xpath fname env in + let f_def = + match func.f_def with + | FBdef d -> d + | _ -> raise (OutlineError OE_InvalidFunc) + in + + (* Get the code from the side we are outlining *) + let code = match side with + | `Left -> goal.es_sl + | `Right -> goal.es_sr + in + + (* Get the return statement and body we will attempt to unify *) + let old_code_body, old_code_ret = + let rest, ret_instr, _ = s_split_i end_pos code in + let body = + if start_pos = end_pos then + s_empty + else + let _, hd, tl = s_split_i start_pos (stmt rest) in + stmt (hd :: tl) + in + + match f_def.f_ret, res_lv with + | None, None -> + s_seq body (stmt [ret_instr]), None + | Some _, Some _ -> + s_seq body (stmt [ret_instr]), None + | Some _, None -> + body, Some ret_instr + | _, _ -> raise (OutlineError OE_UnnecessaryReturn) + in + + (* Get the symbol for each function argument used *) + let arg_names = func.f_sig.fs_anames in + let args = List.filter_map ov_name arg_names in + + (* Insert all the argument symbols we are attempting to unify *) + let umap = List.fold_left (fun umap a -> Msym.add a Empty umap) Msym.empty args in + + (* Unify the function *) + let lv, args_map = unify_func umap f_def old_code_body old_code_ret in + (* Use the correct lv *) + let lv = match lv with | None -> res_lv | _ -> lv in + + (* Check that we were able to unify all arguments *) + let args = + List.map + (fun a -> + match Msym.find a args_map with + | Empty -> raise (OutlineError (OE_UnificationFailure a)) + | Fixed e -> e + ) + args + in + + (* Buid the call statement *) + let proc_call = s_call (lv, fname, args) in + + (* Offload to transitivity *) + t_outline_stmt side start_pos end_pos proc_call tc + +(*---------------------------------------------------------------------------------------*) +(* Process a user call to outline *) + +let process_outline info tc = + let side = info.outline_side in + let start_pos = info.outline_start in + let end_pos = info.outline_end in + + let env = tc1_env tc in + let goal = tc1_as_equivS tc in + let ppe = EcPrinting.PPEnv.ofenv env in + + (* Check which memory we are outlining *) + let mem = match side with + | `Left -> goal.es_ml + | `Right -> goal.es_mr + in + + try + match info.outline_kind with + | OKstmt s -> + let s = EcProofTyping.tc1_process_stmt tc (EcMemory.memtype mem) s in + t_outline_stmt side start_pos end_pos s tc + | OKproc (f, pres_lv) -> + let loc = EcLocation.loc f in + (* Get the function *) + let f = EcTyping.trans_gamepath env f in + let func = EcEnv.Fun.by_xpath f env in + let f_def = + match func.f_def with + | FBdef d -> d + | _ -> raise (OutlineError OE_InvalidFunc) + in + + (* Translate the res_lv if given *) + let res_lv = + match pres_lv, f_def.f_ret with + | Some r, Some e -> begin + try + let subenv = EcEnv.Memory.push_active mem env in + let ue = EcUnify.UniEnv.create (Some []) in + let res = EcTyping.transexpcast subenv `InProc ue e.e_ty r in + let ts = Tuni.subst (EcUnify.UniEnv.close ue) in + let es = e_subst { e_subst_id with es_ty = ts } in + Some (lv_of_expr (es res)) + with EcUnify.UninstanciateUni -> + EcTyping.tyerror loc env EcTyping.FreeTypeVariables + end + | None, _ -> None + | _, _ -> raise (OutlineError OE_UnnecessaryReturn) + in + + t_outline_proc side start_pos end_pos f res_lv tc + with + | OutlineError OE_UnnecessaryReturn -> + tc_error !!tc "outline: left-value given when function does not return" + | OutlineError OE_InvalidFunc -> + tc_error !!tc "outline: cannot outline an abstract function" + | OutlineError (OE_UnificationFailure x) -> + tc_error !!tc "outline: unable to unify `%s`" x + | UnificationError UE_InvalidRetInstr -> + tc_error !!tc ("outline: return instruction kind not supported") + | UnificationError (UE_DifferentProgramLengths (s1, s2)) -> + tc_error !!tc "outline: body's are different lengths\n%a ~ %a" (EcPrinting.pp_stmt ppe) s1 (EcPrinting.pp_stmt ppe) s2 + | UnificationError (UE_InstrNotInLockstep (i1, i2))-> + tc_error !!tc "outline: instructions not in sync\n%a ~ %a" (EcPrinting.pp_instr ppe) i1 (EcPrinting.pp_instr ppe) i2 + | UnificationError (UE_ExprNotInLockstep (e1, e2))-> + tc_error !!tc "outline: expressions not in sync\n%a ~ %a" (EcPrinting.pp_expr ppe) e1 (EcPrinting.pp_expr ppe) e2 diff --git a/src/phl/ecPhlOutline.mli b/src/phl/ecPhlOutline.mli new file mode 100644 index 0000000000..9994ddac32 --- /dev/null +++ b/src/phl/ecPhlOutline.mli @@ -0,0 +1,9 @@ +open EcCoreGoal.FApi +open EcParsetree +open EcModules +open EcPath + +val t_outline_stmt : side -> codepos1 -> codepos1 -> stmt -> backward +val t_outline_proc : side -> codepos1 -> codepos1 -> xpath -> lvalue option -> backward + +val process_outline : outline_info -> backward diff --git a/tests/outline.ec b/tests/outline.ec new file mode 100644 index 0000000000..0781a49a33 --- /dev/null +++ b/tests/outline.ec @@ -0,0 +1,130 @@ +require import AllCore. + +op dint : int distr. + +module M = { + var x : int + + proc f1() : unit = { + M.x <- 0; + } + + proc f2(a: int) : unit = { + M.x <- a; + } + + proc f3(a: int, b: int) : int = { + return a + b; + } + + proc f4(a: int, b: int) : int = { + var t; + if (a <= b) { + t <- b; + } else { + t <- a; + } + return t; + } + + proc f5(d: int distr) : int = { + var v; + v <$ d; + return v; + } +}. + +module N = { + proc g1() : unit = { + M.f1(); + } + + proc g2(a) : unit = { + M.f2(a); + } + + proc g3(a, b) : unit = { + var r; + r <@ M.f3(a, b); + } + + proc g4(a: int, b: int) : unit = { + var m; + if (a <= b) { + m <- b; + } else { + m <- a; + } + M.x <- m; + } + + proc g5() : unit = { + var x; + x <$ dint; + } + + proc g6() : unit = { + var a, b, m; + a <$ dint; + b <$ dint; + if (a <= b) { + m <- b; + } else { + m <- a; + } + M.x <- m; + } +}. + +equiv outline_no_args_no_ret: N.g1 ~ N.g1: true ==> true. +proc. +inline {1} 1. +outline {1} [1] <@ M.f1. +by sim. +qed. + +equiv outline_no_ret: N.g2 ~ N.g2: true ==> true. +proc. +inline {1} 1. +outline {1} [2] <@ M.f2. +by inline*; auto. +qed. + +equiv outline_no_body: N.g3 ~ N.g3: true ==> true. +proc. +inline {1} 1. +outline {1} [3] <@ M.f3. +by inline*; auto. +qed. + +equiv outline_slice: N.g4 ~ N.g4: true ==> true. +proc. +outline {1} [1-2] <@ M.f4. +by inline*; auto. +qed. + +equiv outline_explicit_ret: N.g5 ~ N.g5: true ==> true. +proc. +outline {1} [1] x <@ M.f5. +by inline*; auto. +qed. + +equiv outline_multi: N.g6 ~ N.g6: true ==> true. +proof. +proc. +outline {1} [3-4] <@ N.g4. +outline {1} [2] b <@ M.f5. +outline {1} [1] a <@ M.f5. +by inline*; auto. +qed. + +equiv outline_stmt: N.g6 ~ N.g6: true ==> true. +proof. +proc. +outline {1} [1-4] { + a <@ M.f5(dint); + b <@ M.f5(dint); + N.g4(a,b); +}. +by inline*; auto. +qed.