diff --git a/src/phl/README.md b/src/phl/README.md index e3cfce6dc..9e96a991e 100644 --- a/src/phl/README.md +++ b/src/phl/README.md @@ -83,7 +83,7 @@ Run the test suite with `EC_RECHECK=1` to exercise every migrated checker. ## Program transformations Tactics that replace the program by an equivalent one and keep the judgement -(rndsem, rcond, swap, inline, …) go through **one** trusted +(rndsem, rcond, swap, inline, proc rewrite / change, …) go through **one** trusted transformation rule per logic, `t__transform` (`EcTransform`; equiv: one side at a time), parameterized by an entry of a catalogue: @@ -99,8 +99,11 @@ equiv: one side at a time), parameterized by an entry of a catalogue: function, which may extend the memory with fresh program variables. - The obligations are abstract (a small closed set: so far, "every terminating run of the prefix `hd` from the precondition satisfies - `cond`" and "the statement `ks` is lossless"); each logic's rule states - them as its own premises (see its `.mli`). + `cond`", "the statement `ks` is lossless", "the expressions `e` and + `e'` are equal in every memory" and "the fragments `s` and `s'` are + locally equivalent", the latter's frame being computed by each rule + from its own precondition); each logic's rule states them as its own + premises (see its `.mli`). - The node records the transformation and its parameters; the checker ("-transform") re-runs it on the goal's program and compares the subgoals up to conversion (programs up to alpha-equivalence). @@ -112,7 +115,11 @@ Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`), (`EcTrSetMatch`), `cfold` (`EcTrCFold`), `asgn-case` (`EcTrAsgnCase`), `simplify-if` (`EcTrSimplifyIf`), and the loop transformations `fission` (`EcTrFission`), `fusion` (`EcTrFusion`), `unroll` (`EcTrUnroll`) and -`splitwhile` (`EcTrSplitWhile`). `if-push` / `match-push` push +`splitwhile` (`EcTrSplitWhile`), and the program rewritings +`expr-change` (`EcTrExprChange`, `proc rewrite`), `stmt-change` +(`EcTrStmtChange`, `proc change`), `circuit-change` +(`EcTrCircuitChange`, `proc change circuit`) and `idassign` +(`EcTrIdAssign`). `if-push` / `match-push` push the continuation of a leading conditional / `match` into its branches: the `if` and `match` tactics are push + rule on the conditional alone (`EcIf`, `EcMatch`). diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index dcaeabaf5..306bc7047 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -333,11 +333,11 @@ parameterized by an entry of a **catalogue** of transformations: (`EcPlTransform.register`, a registry of partial handlers like the rule checkers). An entry is a pure, deterministic function of a context and of the statement `c`; it acts at the statement level only and may extend the - memory with fresh program variables. Its context holds the environment, the - memory of `c` and what it needs from the judgement — so far the program - variables read by the postcondition — computed by each logic's rule from its - own judgement, so that the checker recomputes it from the goal (a recorded - set is never trusted). `EcPlTransform.apply` runs an entry, raising + memory with fresh program variables. Its context holds the hypotheses and + environment of the goal, the memory of `c` and what it needs from the + judgement — so far the program variables read by the postcondition — + computed by each logic's rule from its own judgement, so that the checker + recomputes it from the goal (a recorded set is never trusted). `EcPlTransform.apply` runs an entry, raising `InvalidTransform` with a user-facing message when it does not apply. Entries live in `rules/transforms/`, one module `EcTr` each. - **The obligations** are **abstract** and form a small closed set; each @@ -360,6 +360,28 @@ parameterized by an entry of a **catalogue** of transformations: every state; in every logic `phoare [ks : true ==> true] = 1`, in the memory of the transformed program (the premise `kill` has always stated). + - `OExprEq (xs, e, e')`: in every memory of the transformed program's + type and for every value of the local identifiers `xs`, `e` and `e'` + evaluate to the same value; in every logic `forall &m, forall xs, e = + e'`, `&m` named after the program's memory (the premises `proc + rewrite` has always stated, one per rewritten expression). + - `OLocalEquiv (xs, s, s', R, W, M)`: for every value of the match-arm + locals `xs` in scope, from states agreeing on `R` (and satisfying, on + the side of `s`, the frame), the fragment `s` of the program and the + new fragment `s'` end in states agreeing on `W`; in every logic + `forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}]`, left memory + type that of the program, right that of the transformed program (the + premise `proc change` has always stated). The frame `F` is the + obligation depending on the precondition: it is computed by each + rule from its own precondition (`EcPlTransform.frame`), as the + top-level conjuncts of the boolean precondition that only mention the + memory of the program and are independent from `M` (what may be + written before `s` runs): + - hoare, bdhoare: the precondition; + - ehoare: the boolean part `P` of a precondition ``P `|` f``, no frame + otherwise; + - equiv (transformation of side `i`): the relational precondition, + the conjuncts mentioning only the memory of side `i`. - **The rules** `t__transform` (`rules//EcTransform`; equiv: one side at a time, the other program and memory unchanged) record `(transformation, resolved parameters)` (and the side) in their node. The @@ -434,7 +456,31 @@ Current catalogue: for` stays derived: rcond, wp, seq, conseq, cfold); - `splitwhile` (`EcTrSplitWhile`): `while e do c` becomes `while (e /\ b) do c; while e do c`; no obligation; used by - `splitwhile`. + `splitwhile`; +- `expr-change` (`EcTrExprChange`): replaces expressions of a — possibly + nested — range (or of the whole statement), enumerated in program + order, each replacement being stated over identifiers recorded for the + match-arm locals in scope (renamed back in the program, with + type and capture side conditions); obligation `OExprEq` per replaced + expression; used by `proc rewrite` and `proc rewrite /=` in every + logic, which discharge the obligations on the spot; +- `stmt-change` (`EcTrStmtChange`): replaces a — possibly nested — range + by a statement over the memory extended with fresh locals (bound by the + entry with `EcMemory.bindall_fresh`, deterministically); obligation + `OLocalEquiv` between the two fragments, on the variables read by both + and the written variables observable afterwards (by the code that may + run after the range, the postcondition, and, in a loop, the fragments + themselves); used by `proc change` in every logic; +- `circuit-change` (`EcTrCircuitChange`): replaces the `n` instructions + at a — possibly nested — position by a statement over fresh locals, + provided that they are circuit-equivalent (`EcCircuits.instrs_equiv`, + run by the entry, under the context's hypotheses) on the variables + observable afterwards; assignments to local variables only, hence no + `raise` (the entry is sound with exceptional postconditions, whose + variables are observable); no obligation; used by `proc change + circuit` (hoare only); +- `idassign` (`EcTrIdAssign`): inserts `x <- x` at a — possibly nested — + position; no obligation; used by `idassign` (hoare only). The decisions of a conditional or a match are computed by `EcPlRCond`. The `if` and `match` tactics are push + rule on the conditional alone: they @@ -442,7 +488,7 @@ push the continuation into the branches (when there is one) through the transformation rule (on each side, for the two-sided equiv forms), then apply the `if` / `match` rule of their logic (`EcIf`, `EcMatch`), stated on the conditional alone. Further entries come -with the tactics that use them: proc rewrite / change. +with the tactics that use them. Exception: the framed form of `match C k` (used when the variables of the discriminant `e` are neither read nor written by the prefix, and the diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 23d265c11..77089ade7 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -11,14 +11,40 @@ module L = EcLocation module PT = EcProofTerm (* -------------------------------------------------------------------- *) -(* The match-arm locals in scope at the end of [path], outermost first. *) -let rec locals_of_path (path : EcMatching.Zipper.ipath) = - match path with - | ZTop -> [] - | ZWhile (_, (_, path)) - | ZIfThen (_, (_, path), _) - | ZIfElse (_, _, (_, path)) -> locals_of_path path - | ZMatch (_, (_, path), ctxt) -> locals_of_path path @ ctxt.locals +(* [proc rewrite] and [proc change] are derived, uniformly in every logic + (hoare, ehoare, phoare, and equiv on one side): they resolve their + arguments, check what they always checked (keeping their error + messages), and apply a program transformation of the catalogue + ([EcTrExprChange], [EcTrStmtChange]) through the transformation rule of + the logic of the goal ([EcTransform]). The visible goals are + those of that rule: the obligations of the transformation, then the + transformed judgement. + - [proc rewrite] (and [proc rewrite /=]): [EcTrExprChange], one + equality [forall &m, forall locals, e = e'] per rewritten expression + (in program order), each discharged on the spot by the tactic; + - [proc change]: [EcTrStmtChange], one local equivalence between the + replaced fragment and the new one (its frame computed by the rule + from its precondition), left to the user. + As they only differ by the transformation they apply, they share the + logic-agnostic dispatcher [t_transform] below, and no per-logic module. + [proc rewrite pre] is derived from [conseq]. *) + +(* -------------------------------------------------------------------- *) +(* Apply the transformation [tr] through the transformation rule of the + logic of the goal (on the given side for equiv). *) +let t_transform (side : side option) (tr : EcPlTransform.transform) (tc : tcenv1) = + match side, (FApi.tc1_goal tc).f_node with + | None, FhoareS _ -> + EcHoareTransform.t_hoare_transform { htr_tr = tr } tc + | None, FeHoareS _ -> + EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr } tc + | None, FbdHoareS _ -> + EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr } tc + | Some side, FequivS _ -> + EcEquivTransform.t_equiv_transform { etr_side = side; etr_tr = tr } tc + | _ -> + EcLowPhlGoal.tc_error_noXhl + ~kinds:(EcLowPhlGoal.hlkinds_Xhl_r `Stmt) !!tc (* -------------------------------------------------------------------- *) (* [t_change_range side range expr tc] applies [expr] to every expression @@ -27,10 +53,12 @@ let rec locals_of_path (path : EcMatching.Zipper.ipath) = [expr] receives the hypotheses extended with the match-arm locals in scope and returns [None] to leave an expression untouched. - One equality side goal is emitted per rewritten expression, in program - order, followed by the rewritten program-logic goal. Each side goal is - of the form [forall &m, forall locals, e = e'] and is returned along - with the identifiers to introduce to reach the equality. *) + The expressions are enumerated as [EcTrExprChange] does; the + replacements are applied by that transformation, which emits one + equality side goal per rewritten expression, in program order, + followed by the rewritten program-logic goal. Each side goal is of the + form [forall &m, forall locals, e = e'] and is returned along with the + identifiers to introduce to reach the equality. *) let t_change_range (side : side option) (range : EcMatching.Position.codegap_range option) @@ -51,7 +79,7 @@ let t_change_range let mid = EcMemory.memory m in (* Match-arm locals are renamed apart from the hypotheses for the side - goal; the program keeps its own binders. *) + goal; the transformation renames them back in the program. *) let change (locals : (EcIdent.t * ty) list) acc (e : expr) = let ids = LDecl.fresh_ids hyps (List.map (fun (x, _) -> EcIdent.name x) locals) in @@ -61,54 +89,44 @@ let t_change_range (fun hyps (id, ty) -> LDecl.add_local id (LD_var (ty, None)) hyps) hyps fresh in - let rename (froms : (EcIdent.t * ty) list) (tos : (EcIdent.t * ty) list) = - let subst = - List.fold_left2 - (fun subst (x, _) (y, ty) -> - EcCoreSubst.bind_elocal subst x (EcTypes.e_local y ty)) - EcCoreSubst.Fsubst.f_subst_id froms tos - in EcCoreSubst.e_subst subst in - - let e = rename locals fresh e in + let subst = + List.fold_left2 + (fun subst (x, _) (y, ty) -> + EcCoreSubst.bind_elocal subst x (EcTypes.e_local y ty)) + EcCoreSubst.Fsubst.f_subst_id locals fresh in - match expr e (hyps, m) with + match expr (EcCoreSubst.e_subst subst e) (hyps, m) with | None -> - acc, rename fresh locals e + (None, None) :: acc, e | Some (data, e') -> - let f = ss_inv_of_expr mid e in - let f' = ss_inv_of_expr mid e' in - let goal = map_ss_inv2 f_eq f f' in - let goal = - map_ss_inv1 - (f_forall (List.map (fun (x, ty) -> (x, GTty ty)) fresh)) - goal in - let goal = EcSubst.f_forall_mems_ss_inv m goal in - ((data, mid :: ids), goal) :: acc, rename fresh locals e' + (Some (ids, e'), Some (data, mid :: ids)) :: acc, e in - let acc, s = + let trange, acc = match range with | None -> - s_fold_map_expr change [] s + None, fst (EcTrExprChange.exprs change [] s.s_node) | Some range -> - let zpr, (_, body, epilog), _ = + let zpr, (_, body, _), nmr = try EcMatching.Zipper.zipper_and_split_of_cgap_range env range s with EcMatching.Position.InvalidCPos -> tc_error !!tc "invalid code position" in - let locals = locals_of_path zpr.z_path in - let acc, body = - List.fold_left_map (i_fold_map_expr ~locals change) [] body in - acc, EcMatching.Zipper.zip { zpr with z_tail = body @ epilog } + let locals = EcTrExprChange.locals_of_path zpr.z_path in + Some nmr, fst (EcTrExprChange.exprs ~locals change [] body) in - let data, goals = List.split (List.rev acc) in - let concl = EcLowPhlGoal.hl_set_stmt side concl s in + let changes, data = List.split (List.rev acc) in + let data = List.pmap identity data in - data, FApi.xmutate1 tc `ProcChange (goals @ [concl]) + data, + t_transform side + (EcTrExprChange.TrExprChange + { trec_range = trange; trec_exprs = changes; }) + tc (* -------------------------------------------------------------------- *) let try_rewrite_patterns @@ -295,172 +313,35 @@ let process_rewrite_at |> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id] (* -------------------------------------------------------------------- *) -(* [t_change_stmt side pos ?mt s] replaces a code range with [s] by - generating: +(* [t_change_stmt side pos binds s] replaces a code range with [s] (typed + in the memory extended with the fresh locals [binds], as bound by + [EcMemory.bindall_fresh]) through [EcTrStmtChange], generating: - a local equivalence goal showing that the original fragment and [s] agree under the framed precondition on the variables they both read, and produce the same values for everything observable afterwards; - - the original program-logic goal with the selected range rewritten. - - If [mt] is provided, it is used as the memtype of the selected side (e.g. - when fresh local variables have been bound); otherwise, the memtype is - taken from the goal. *) + - the original program-logic goal with the selected range rewritten. *) let t_change_stmt - (side : side option) - (pos : EcMatching.Position.codegap_range) - ?(mt : memtype option) - (s : stmt) - (tc : tcenv1) + (side : side option) + (pos : EcMatching.Position.codegap_range) + (binds : ovariable list) + (s : stmt) + (tc : tcenv1) = let env = FApi.tc1_env tc in - let (mid, metc), stmt = EcLowPhlGoal.tc1_get_stmt side tc in - let mt = odfl metc mt in + let _, stmt = EcLowPhlGoal.tc1_get_stmt side tc in - let zpr, (_,stmt, epilog), _nmr = + let _, _, nmr = try EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt with EcMatching.Position.InvalidCPos -> tc_error !!tc "invalid code position" in - (* Inside a loop, the fragment may run several times. Its later runs - start after the surrounding code of the loop, but also after the - previous runs of the fragment itself, and from states where the two - programs only agree on the observable variables (see [obs] below). *) - let inloop = EcMatching.Zipper.in_loop zpr.z_path in - - (* Collect the variables that may be modified before (a run of) the - fragment: by the surrounding context and, inside a loop, by the - previous runs of the original fragment. *) - let modi = - let zpr = { zpr with z_tail = epilog } in - let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in - let modi = EcPV.zpr_pv `Write `Before env EcPV.PV.empty zpr in - if inloop then EcPV.is_write_r env modi stmt else modi in - - (* Keep only the top-level conjuncts of the current precondition that talk - about the active memory and are independent from the surrounding writes. - The precondition of an ehoare goal is real-valued: only its boolean - part [P], when it has the form [P `|` f], can be framed. *) - let frame = - let filter (f : form) = - let pvs = EcPV.form_read env EcPV.PMVS.empty f in - let pvs_me = EcIdent.Mid.find_def EcPV.PV.empty mid pvs in - let pvs = EcIdent.Mid.remove mid pvs in - - EcIdent.Mid.is_empty pvs - && (EcPV.PV.indep env modi pvs_me) in - - let pre = - let pre = inv_of_inv (EcLowPhlGoal.tc1_get_pre tc) in - match (FApi.tc1_goal tc).f_node with - | FeHoareS _ -> begin - match destr_app pre with - | o, [p; _] when f_equal o fop_interp_ehoare_form -> Some p - | _ -> None - end - | _ -> Some pre in - - obind (EcFol.filter_topand_form filter) pre in - - let written = EcPV.PV.empty in - let written = EcPV.is_write_r env written stmt in - let written = EcPV.is_write_r env written s.s_node in - - (* The observable variables: those read by the code that may run after - the fragment (for an enclosing loop, its guard and its whole body) - and by the postcondition. Inside a loop, we add the variables read - by both fragments, i.e. the ones assumed equal by the local - equivalence below. - Soundness: the original and new programs are related by "the states - agree on [obs]" (they are equal before the first run of the - fragment). The code after the fragment only reads [obs], so it - preserves this relation. When reaching the fragment, the relation - implies the equalities of the precondition of the local - equivalence (their variables are in [obs] when in a loop), the - frame holds on the original side as no code run so far writes its - variables (see [modi]), and the local equivalence then - re-establishes the relation: the observable variables that are - written are equal, and the other ones are unchanged. *) - let obs = - let zpr = { zpr with z_tail = epilog } in - let zpr = (zpr.z_head, zpr.z_tail), zpr.z_path in - let obs = EcPV.zpr_pv `Read `After env EcPV.PV.empty zpr in - let obs = - if inloop then - EcPV.PV.union obs - (EcPV.PV.inter (EcPV.is_read env stmt) (EcPV.is_read env s.s_node)) - else obs in - - let goal = - let pvs = - EcLowPhlGoal.logicS_post_read env - (EcLowPhlGoal.get_logicS (FApi.tc1_goal tc)) - in - EcIdent.Mid.find_def EcPV.PV.empty mid pvs - in - - EcPV.PV.union obs goal - in - - let written = EcPV.PV.inter written obs in - - (* The local equivalence goal relates shared reads in the precondition and - the writes that remain observable in the continuation/postcondition. *) - let wr_pvs, wr_globs = EcPV.PV.elements written in - - let pr_pvs, pr_globs = EcPV.PV.elements @@ EcPV.PV.inter - (EcPV.is_read env stmt) - (EcPV.is_read env s.s_node) - in - - let ml = EcIdent.create "&1" in - let mr = EcIdent.create "&2" in - - let frame = omap (fun frame -> - let subst = EcSubst.add_memory EcSubst.empty mid ml in - EcSubst.subst_form subst frame) frame in - - let mk_pv_eq ((pv, ty) : prog_var * ty) = - f_eq (f_pvar pv ty ml).inv (f_pvar pv ty mr).inv - - and mk_glob_eq (mp : EcPath.mpath) = - f_eqglob mp ml mp mr - - in - - let pr_eq = List.map mk_pv_eq pr_pvs @ List.map mk_glob_eq pr_globs in - let po_eq = List.map mk_pv_eq wr_pvs @ List.map mk_glob_eq wr_globs in - - (* First subgoal: prove that the replacement fragment preserves the - observable behavior required by the outer proof. The left program is the - original fragment, which only mentions the pre-existing locals - ([metc]); the right program is the replacement, which may use the - freshly bound locals ([mt]). Inside the arm of a [match], the original - fragment may mention the locals bound by the arm: the subgoal is - quantified over them, as the fragment runs for any of their values. *) - let goal1 = - f_forall - (List.map (fun (x, ty) -> (x, GTty ty)) (locals_of_path zpr.z_path)) - (f_equivS - metc mt - { ml; mr; inv = ofold f_and (f_ands pr_eq) frame; } - (EcAst.stmt stmt) s - { ml; mr; inv = f_ands po_eq; }) - in - - let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in - - (* Second subgoal: continue with the original goal after rewriting the - selected statement range. The rewritten side also takes [mt], as the new - statement may mention the fresh locals. *) - let goal2 = - EcLowPhlGoal.hl_set_stmt - ~mt side (FApi.tc1_goal tc) - stmt in - - FApi.xmutate1 tc `ProcChangeStmt [goal1; goal2] + t_transform side + (EcTrStmtChange.TrStmtChange + { trsc_range = nmr; trsc_binds = binds; trsc_stmt = s; }) + tc (* -------------------------------------------------------------------- *) let process_change_stmt @@ -514,4 +395,4 @@ let process_change_stmt let hyps = EcEnv.LDecl.push_active_ss me hyps in let s = EcProofTyping.process_stmt hyps s in - t_change_stmt side pos ~mt:(snd me) s tc + t_change_stmt side pos bindings s tc diff --git a/src/phl/ecPhlRwPrgm.ml b/src/phl/ecPhlRwPrgm.ml index d19e4a072..c17d372b1 100644 --- a/src/phl/ecPhlRwPrgm.ml +++ b/src/phl/ecPhlRwPrgm.ml @@ -3,7 +3,17 @@ open EcUtils open EcAst open EcParsetree open EcCoreGoal -open EcLowPhlGoal + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* The rw_prgm tactics are derived, hoare only: they resolve their + arguments, check what they always checked (keeping their error + messages), and apply a program transformation of the catalogue through + the hoare transformation rule ([EcHoareTransform]): + - [proc change circuit]: [EcTrCircuitChange] (the circuit-equivalence + check is made by the transformation; no obligation); + - [idassign]: [EcTrIdAssign] (no obligation). *) (* -------------------------------------------------------------------- *) type change_t = pcodepos * ptybindings option * int * pstmt @@ -18,7 +28,7 @@ let process_change ((cpos, bindings, i, s) : change_t) (tc : tcenv1) = if not (POE.is_empty (hs_po hs).hsi_inv) then tc_error !!tc "exceptions not supported"; - let mem, _ = + let mem, binds = let bindings = bindings |> Option.value ~default:[] @@ -34,11 +44,9 @@ let process_change ((cpos, bindings, i, s) : change_t) (tc : tcenv1) = let x = Option.map EcLocation.unloc (EcLocation.unloc x) in let vr = EcAst.{ ov_name = x; ov_type = ty; } in let (mem, _) = EcMemory.bind_fresh vr mem in - let x = match x with - | Some x -> x - | None -> tc_error !!tc "Missing name for variable" - in - (mem, (EcTypes.pv_loc x, ty)) + if Option.is_none x then + tc_error !!tc "Missing name for variable"; + (mem, vr) ) hs.hs_m bindings in let env = EcEnv.Memory.push_active_ss mem env in @@ -53,64 +61,16 @@ let process_change ((cpos, bindings, i, s) : change_t) (tc : tcenv1) = let sb = EcCoreSubst.Tuni.subst (EcUnify.UniEnv.close ue) in EcCoreSubst.s_subst sb s in - let zp = Zpr.zipper_of_cpos env cpos hs.hs_s in - - let zp = - let target, tl = List.split_at i zp.z_tail in - - (* [keep] is the set of variables on which [target] and [s] must - agree. Let [R] be the variables read by both [target] and [s]. - We take for [keep]: - - the variables read by the code that may run after the fragment - (for each enclosing [while], its guard and its whole body), - and by the postcondition; - - if the fragment is inside a loop, [R]. - Soundness: the original and the new programs are related by - "the states agree on [keep]" (they are equal before the first - run of the fragment). The code that may run after the fragment - only reads [keep], so preserves this relation. When reaching the - fragment in states [m1] (original) and [m2] (new), let [m] be - [m2] updated with the values of [m1] on [read(target) \ R]. - Then [m] agrees with [m1] on [read(target)] and on [keep] (as - [R] is included in [keep]), and with [m2] on [read(s)] and on - [keep]. As [target] and [s] are deterministic, we get - [target(m1) =keep target(m) =keep s(m) =keep s(m2)], the middle - equality being the one established by the circuit checker. - Outside a loop, the fragment is run once, from [m1 = m2], and - [R] does not need to be kept. *) - let keep = - let zpr = ((zp.z_head, tl), zp.z_path) in - EcPV.zpr_pv `Read `After env EcPV.PV.empty zpr in - let keep = - if Zpr.in_loop zp.z_path then - EcPV.PV.union keep - (EcPV.PV.inter - (EcPV.is_read env target) - (EcPV.is_read env s.s_node)) - else keep in - let keep = EcPV.PV.union keep (EcPV.PV.fv env (EcMemory.memory mem) (POE.lower (EcAst.hs_po hs)).inv) in - (* The variables that are neither read nor written by [target] and - [s] are left unchanged by both and need not be compared. This - drops the global variables, which [target] and [s] cannot access - (this is checked by the circuit checker). *) - let keep = - let ts = target @ s.s_node in - EcPV.PV.inter keep - (EcPV.PV.union (EcPV.is_read env ts) (EcPV.is_write env ts)) in - let st = EcLowCircuits.create_state (EcEnv.gstate env) in - - let equiv = - try EcCircuits.instrs_equiv (FApi.tc1_hyps tc) ~keep mem st target s.s_node - with e -> - tc_error !!tc "circuit-equivalence checker error: %s" (Printexc.to_string e) - in - if not equiv then - tc_error !!tc "statements are not circuit-equivalent"; - { zp with z_tail = s.s_node @ tl } in - - let hs = { hs with hs_s = Zpr.zip zp; hs_m = mem; } in - - FApi.xmutate1 tc `BChange EcAst.[EcFol.f_hoareS (hs.hs_m |> snd) (hs_pr hs) (hs.hs_s) (hs_po hs)] + let zp, (at, _) = Zpr.zipper_of_cpos_r env cpos hs.hs_s in + + (* Fails (with [Invalid_argument]) when there are fewer than [i] + instructions at the position. *) + ignore (List.split_at i zp.z_tail : _ * _); + + EcHoareTransform.t_hoare_transform + { htr_tr = EcTrCircuitChange.TrCircuitChange + { trcc_at = at; trcc_len = i; trcc_binds = binds; trcc_stmt = s; } } + tc (* -------------------------------------------------------------------- *) type idassign_t = pcodepos * pqsymbol @@ -122,14 +82,12 @@ let process_idassign ((cpos, pv) : idassign_t) (tc : tcenv1) = let env = EcEnv.Memory.push_active_ss hs.hs_m env in let cpos = EcTyping.trans_codepos env cpos in - let pv, pvty = EcTyping.trans_pv env pv in - let sasgn = EcModules.i_asgn (LvVar (pv, pvty), EcTypes.e_var pv pvty) in - let hs = - let s = Zpr.zipper_of_cpos env cpos hs.hs_s in - let s = { s with z_tail = sasgn :: s.z_tail } in - { hs with hs_s = Zpr.zip s } in - FApi.xmutate1 tc `IdAssign - [EcFol.f_hoareS (snd hs.hs_m) (hs_pr hs) (hs.hs_s) (hs_po hs)] + let pv = EcTyping.trans_pv env pv in + let _, (at, _) = Zpr.zipper_of_cpos_r env cpos hs.hs_s in + + EcHoareTransform.t_hoare_transform + { htr_tr = EcTrIdAssign.TrIdAssign { tria_at = at; tria_pv = pv; } } + tc (* -------------------------------------------------------------------- *) let process_rw_prgm (mode : rwprgm) (tc : tcenv1) = diff --git a/src/phl/rules/bdhoare/ecBdHoareTransform.ml b/src/phl/rules/bdhoare/ecBdHoareTransform.ml index d6e1cdecc..15c20a402 100644 --- a/src/phl/rules/bdhoare/ecBdHoareTransform.ml +++ b/src/phl/rules/bdhoare/ecBdHoareTransform.ml @@ -29,6 +29,7 @@ let bdhoare_transform_subgoals let env = LDecl.toenv hyps in let m = fst bhs.bhs_m in let ctxt = { + trc_hyps = hyps; trc_env = env; trc_me = bhs.bhs_m; trc_post = lazy (EcPV.PV.fv env m (bhs_po bhs).inv); @@ -41,7 +42,11 @@ let bdhoare_transform_subgoals f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd (POE.lift cond) | OLossless ks -> f_bdHoareS (snd bhs.bhs_m) - { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } + | OExprEq o -> + f_expr_eq r.trr_me o + | OLocalEquiv o -> + f_local_equiv env bhs.bhs_m (snd r.trr_me) (Some (bhs_pr bhs).inv) o in List.map obligation r.trr_obl @ [f_bdHoareS (snd r.trr_me) (bhs_pr bhs) r.trr_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs)] diff --git a/src/phl/rules/bdhoare/ecBdHoareTransform.mli b/src/phl/rules/bdhoare/ecBdHoareTransform.mli index d3755035a..53c8025b6 100644 --- a/src/phl/rules/bdhoare/ecBdHoareTransform.mli +++ b/src/phl/rules/bdhoare/ecBdHoareTransform.mli @@ -18,11 +18,21 @@ type bdhoare_transform = { phoare [c : P ==> Q] ~ d where [c'] may live in an extended memory (fresh program variables), - and the entry is given the program variables read by [Q]. Each - obligation becomes a premise (first, in order): + and the entry is given the goal's hypotheses and the program variables + read by [Q]. Each obligation becomes a premise (first, in order): - [OPrefixPost (hd, cond)]: hoare [hd : P ==> cond]; - [OLossless ks]: phoare [ks : true ==> true] = 1 - (in the memory of [c]). + (in the memory of [c]); + - [OExprEq (xs, e, e')]: forall &m, forall xs, e = e' + ([&m] the memory of [c'], named after the goal's); + - [OLocalEquiv (xs, s, s', R, W, M)]: + forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}] + (left: the memory of [c], right: that of [c']), the frame [F] being + the conjunction of the top-level conjuncts of [P] that only mention + the memory of [c] and are independent from [M] + ([EcPlTransform.frame]). + The variables read by the bound [d] are not given to the entry: [d] is + evaluated in the initial memory. Side condition: [t] applies to [c] (otherwise fails with its message). Node: [RBdHoareTransform { btr_tr = t }]. Checker: "bdhoare-transform" diff --git a/src/phl/rules/ecPlTransform.ml b/src/phl/rules/ecPlTransform.ml index 6b869555e..6509d6807 100644 --- a/src/phl/rules/ecPlTransform.ml +++ b/src/phl/rules/ecPlTransform.ml @@ -12,13 +12,31 @@ type transform = .. type obligation = | OPrefixPost of prefix_post | OLossless of stmt + | OExprEq of expr_eq + | OLocalEquiv of local_equiv and prefix_post = { opp_prefix : stmt; opp_cond : ss_inv; } +and expr_eq = { + oee_locals : (EcIdent.t * ty) list; + oee_lhs : expr; + oee_rhs : expr; +} + +and local_equiv = { + ole_locals : (EcIdent.t * ty) list; + ole_orig : stmt; + ole_new : stmt; + ole_reads : EcPV.PV.t; + ole_writes : EcPV.PV.t; + ole_modi : EcPV.PV.t; +} + type tr_ctxt = { + trc_hyps : LDecl.hyps; trc_env : env; trc_me : memenv; trc_post : EcPV.PV.t Lazy.t; @@ -46,3 +64,55 @@ let apply (ctxt : tr_ctxt) (t : transform) (s : stmt) = match List.find_map (fun f -> f t) !entries with | None -> raise (InvalidTransform "unknown program transformation") | Some run -> run ctxt s + +(* -------------------------------------------------------------------- *) +(* The frame of a local equivalence: the top-level conjuncts of the + precondition that only talk about the memory [m] and are independent + from [modi], i.e. that still hold when the fragment runs. *) +let frame (env : env) (m : memory) (modi : EcPV.PV.t) (pre : form) = + let filter (f : form) = + let pvs = EcPV.form_read env EcPV.PMVS.empty f in + let pvs_me = EcIdent.Mid.find_def EcPV.PV.empty m pvs in + let pvs = EcIdent.Mid.remove m pvs in + + EcIdent.Mid.is_empty pvs + && EcPV.PV.indep env modi pvs_me in + + EcFol.filter_topand_form filter pre + +(* -------------------------------------------------------------------- *) +let f_expr_eq (me : memenv) (o : expr_eq) = + let m = fst me in + let f = EcFol.ss_inv_of_expr m o.oee_lhs in + let f' = EcFol.ss_inv_of_expr m o.oee_rhs in + let bd = List.map (fun (x, ty) -> (x, GTty ty)) o.oee_locals in + EcSubst.f_forall_mems_ss_inv me + (map_ss_inv1 (EcFol.f_forall bd) (map_ss_inv2 EcFol.f_eq f f')) + +(* -------------------------------------------------------------------- *) +(* The original fragment runs in [&1], over the memory type of [me], the + new one in [&2], over [mt']; the frame is read on [&1]. *) +let f_local_equiv + (env : env) (me : memenv) (mt' : memtype) (pre : form option) + (o : local_equiv) += + let ml = EcIdent.create "&1" in + let mr = EcIdent.create "&2" in + + let frame = + EcUtils.obind (frame env (fst me) o.ole_modi) pre + |> EcUtils.omap (fun frame -> + let subst = EcSubst.add_memory EcSubst.empty (fst me) ml in + EcSubst.subst_form subst frame) in + + let eqs (pvs : EcPV.PV.t) = + let pvs, globs = EcPV.PV.elements pvs in + List.map (fun (pv, ty) -> EcFol.f_eq (EcFol.f_pvar pv ty ml).inv (EcFol.f_pvar pv ty mr).inv) pvs + @ List.map (fun mp -> EcFol.f_eqglob mp ml mp mr) globs in + + EcFol.f_forall + (List.map (fun (x, ty) -> (x, GTty ty)) o.ole_locals) + (EcFol.f_equivS (snd me) mt' + { ml; mr; inv = EcUtils.ofold EcFol.f_and (EcFol.f_ands (eqs o.ole_reads)) frame; } + o.ole_orig o.ole_new + { ml; mr; inv = EcFol.f_ands (eqs o.ole_writes); }) diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index 58710be7a..ba5d21214 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -38,8 +38,12 @@ open EcEnv [EcTrAlias], [EcTrSet], [EcTrSetMatch], [EcTrCFold], [EcTrAsgnCase] and [EcTrSimplifyIf] (the code transformations), [EcTrFission] / [EcTrFusion] (splitting / merging loops), [EcTrUnroll] (unrolling the - first iteration of a loop) and [EcTrSplitWhile] (splitting a loop on an - extra condition). Entries live + first iteration of a loop), [EcTrSplitWhile] (splitting a loop on an + extra condition), [EcTrExprChange] (replacing expressions under + equalities, [proc rewrite]), [EcTrStmtChange] (replacing a fragment + under a local equivalence, [proc change]), [EcTrCircuitChange] + (replacing a fragment by a circuit-equivalent one, [proc change + circuit]) and [EcTrIdAssign] (inserting [x <- x]). Entries live in [rules/transforms/], as [EcTr]. The framed form of [match C k] changes the precondition: it is not a transformation, but a separate rule of each logic ([EcRMatch]). *) @@ -50,27 +54,58 @@ type transform = .. (* An obligation of a transformation, about the program [c] it is applied to, in the memory of the context (the memory of [c], not the possibly - extended one of [c']). *) + extended one of [c']), unless stated otherwise. *) type obligation = | OPrefixPost of prefix_post | OLossless of stmt + | OExprEq of expr_eq + | OLocalEquiv of local_equiv (* [OPrefixPost { opp_prefix = hd; opp_cond = cond }]: every terminating run of [hd] (a prefix of [c]) from the precondition ends in a state satisfying [cond]. [OLossless ks]: the statement [ks] (a fragment of [c], over its memory) - terminates with probability 1 from every state. *) + terminates with probability 1 from every state. + + [OExprEq { oee_locals = xs; oee_lhs = e; oee_rhs = e' }]: in every + memory of the type of [c'] and for every value of the local + identifiers [xs], [e] and [e'] evaluate to the same value ([e] and + [e'] are over the memory of [c'], the [xs] free). + + [OLocalEquiv { ole_locals = xs; ole_orig = s; ole_new = s'; + ole_reads = R; ole_writes = W; ole_modi = M }]: for every value of the + match-arm locals [xs] in scope at [s] (which [s] may mention), from + states agreeing on [R] (and, on the side of [s], satisfying the frame: + the part of the precondition independent from [M], see [frame] below), + the fragment [s] of [c] (over the memory of [c]) and the fragment [s'] + (over the memory of [c']) end in states agreeing on [W]. *) and prefix_post = { opp_prefix : stmt; (* the prefix [hd] *) opp_cond : ss_inv; (* [cond] *) } +and expr_eq = { + oee_locals : (EcIdent.t * ty) list; (* the locals [xs], with their types *) + oee_lhs : expr; (* [e] *) + oee_rhs : expr; (* [e'] *) +} + +and local_equiv = { + ole_locals : (EcIdent.t * ty) list; (* the arm locals [xs] in scope *) + ole_orig : stmt; (* the original fragment [s] *) + ole_new : stmt; (* the new fragment [s'] *) + ole_reads : EcPV.PV.t; (* the shared reads [R] *) + ole_writes : EcPV.PV.t; (* the observable writes [W] *) + ole_modi : EcPV.PV.t; (* [M]: what may be written before [s] runs *) +} + (* What an entry is given, besides the statement: computed by each logic's rule from its own judgement (so that the checker recomputes it from the goal). *) type tr_ctxt = { - trc_env : env; (* environment of the goal *) + trc_hyps : LDecl.hyps; (* hypotheses of the goal *) + trc_env : env; (* its environment *) trc_me : memenv; (* memory of the transformed program *) trc_post : EcPV.PV.t Lazy.t; (* program variables of [trc_me] read by the postcondition (for hoare, @@ -103,3 +138,30 @@ val register : (transform -> (tr_ctxt -> stmt -> tr_result) option) -> unit (* [apply ctxt t c] runs the entry of [t] on [c]. Raises [InvalidTransform] when it does not apply (or no entry handles [t]). *) val apply : tr_ctxt -> transform -> stmt -> tr_result + +(* -------------------------------------------------------------------- *) +(* Premises shared by the transformation rules of every logic. *) + +(* [frame env m modi pre]: the conjunction of the top-level conjuncts of + the boolean precondition [pre] that only mention the memory [m] (of the + transformed program) and are independent from the program variables + [modi]; [None] when there is none. *) +val frame : env -> memory -> EcPV.PV.t -> form -> form option + +(* [f_expr_eq me o]: the premise of [OExprEq o] in every logic, + [forall &m, forall xs, e = e'], the memory binder being the memory + identifier of [me] (the memory of the transformed program) and the + local binders the identifiers [xs] of [o]. *) +val f_expr_eq : memenv -> expr_eq -> form + +(* [f_local_equiv env me mt' pre o]: the premise of [OLocalEquiv o] in + every logic, + + forall xs, equiv [s ~ s' : ={R} /\ frame{1} ==> ={W}] + + with left memory type that of [me] (the memory of [c]), right memory + type [mt'] (the memory type of [c']), and [frame] computed by [frame] + from the boolean precondition [pre] of the rule over the memory of [me] + (no frame when [pre] is [None]). *) +val f_local_equiv : + env -> memenv -> memtype -> form option -> local_equiv -> form diff --git a/src/phl/rules/ehoare/ecEHoareTransform.ml b/src/phl/rules/ehoare/ecEHoareTransform.ml index 390e6ba59..5a01373f4 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.ml +++ b/src/phl/rules/ehoare/ecEHoareTransform.ml @@ -21,34 +21,43 @@ type EcCoreGoal.rule += REHoareTransform of ehoare_transform (* -------------------------------------------------------------------- *) (* Pure core shared by the rule and its checker: run the transformation on the goal's program, then state its obligations (first, in order) and the - transformed judgement. The obligations are hoare judgements from the - boolean part [P] of the precondition [P `|` f], which must have that - form when there is an obligation. *) + transformed judgement. The prefix obligations are hoare judgements from + the boolean part [P] of the precondition [P `|` f], which must have that + form when there is one; the frame of a local equivalence is taken from + [P] when the precondition has that form (no frame otherwise). *) let ehoare_transform_subgoals (hyps : LDecl.hyps) (hs : eHoareS) (n : ehoare_transform) = let env = LDecl.toenv hyps in let m = fst hs.ehs_m in let ctxt = { + trc_hyps = hyps; trc_env = env; trc_me = hs.ehs_m; trc_post = lazy (EcPV.PV.fv env m (ehs_po hs).inv); trc_exn = false; } in let r = apply ctxt n.ehtr_tr hs.ehs_s in + let bool_pre = + match destr_app (ehs_pr hs).inv with + | o, pre :: _ when f_equal o fop_interp_ehoare_form -> Some pre + | _ -> None in let pre () = - let pre pr = - match destr_app pr with - | o, pre :: _ when f_equal o fop_interp_ehoare_form -> pre - | _ -> raise (InvalidTransform "the pre should have the form \"_ `|` _\"") in - map_ss_inv1 pre (ehs_pr hs) in + match bool_pre with + | Some pre -> { (ehs_pr hs) with inv = pre } + | None -> + raise (InvalidTransform "the pre should have the form \"_ `|` _\"") in let obligation = function | OPrefixPost { opp_prefix = hd; opp_cond = cond } -> let cond = { (ss_inv_rebind cond m) with m } in f_hoareS (snd hs.ehs_m) (pre ()) hd (POE.lift cond) | OLossless ks -> f_bdHoareS (snd hs.ehs_m) - { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } + | OExprEq o -> + f_expr_eq r.trr_me o + | OLocalEquiv o -> + f_local_equiv env hs.ehs_m (snd r.trr_me) bool_pre o in List.map obligation r.trr_obl @ [f_eHoareS (snd r.trr_me) (ehs_pr hs) r.trr_s (ehs_po hs)] diff --git a/src/phl/rules/ehoare/ecEHoareTransform.mli b/src/phl/rules/ehoare/ecEHoareTransform.mli index 2f07babce..d7eed542e 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.mli +++ b/src/phl/rules/ehoare/ecEHoareTransform.mli @@ -17,13 +17,22 @@ type ehoare_transform = { ehoare [c : P ==> Q] where [c'] may live in an extended memory (fresh program variables), - and the entry is given the program variables read by [Q]. Each - obligation becomes a premise (first, in order): + and the entry is given the goal's hypotheses and the program variables + read by [Q]. Each obligation becomes a premise (first, in order): - [OPrefixPost (hd, cond)]: hoare [hd : P_bool ==> cond] where [P] is [P_bool `|` f] (otherwise fails with "the pre should have the form \"_ `|` _\""); - [OLossless ks]: phoare [ks : true ==> true] = 1 - (in the memory of [c]). + (in the memory of [c]); + - [OExprEq (xs, e, e')]: forall &m, forall xs, e = e' + ([&m] the memory of [c'], named after the goal's); + - [OLocalEquiv (xs, s, s', R, W, M)]: + forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}] + (left: the memory of [c], right: that of [c']), the frame [F] being + the conjunction of the top-level conjuncts of [P_bool] that only + mention the memory of [c] and are independent from [M] + ([EcPlTransform.frame]) when [P] is [P_bool `|` f], and no frame + otherwise. Side condition: [t] applies to [c] (otherwise fails with its message). Node: [REHoareTransform { ehtr_tr = t }]. Checker: "ehoare-transform" diff --git a/src/phl/rules/equiv/ecEquivTransform.ml b/src/phl/rules/equiv/ecEquivTransform.ml index bcb5b6c05..b761dd403 100644 --- a/src/phl/rules/equiv/ecEquivTransform.ml +++ b/src/phl/rules/equiv/ecEquivTransform.ml @@ -37,6 +37,7 @@ let equiv_transform_subgoals | `Right -> es.es_mr, es.es_ml, es.es_sr in let m = fst me in let ctxt = { + trc_hyps = hyps; trc_env = env; trc_me = me; trc_post = lazy (EcPV.PV.fv env m (es_po es).inv); @@ -59,7 +60,11 @@ let equiv_transform_subgoals f_hoareS (snd me) pr hd (POE.lift po)) (es_pr es) cond) | OLossless ks -> f_bdHoareS (snd me) - { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } + | OExprEq o -> + f_expr_eq r.trr_me o + | OLocalEquiv o -> + f_local_equiv env me (snd r.trr_me) (Some (es_pr es).inv) o in let concl = match side with | `Left -> diff --git a/src/phl/rules/equiv/ecEquivTransform.mli b/src/phl/rules/equiv/ecEquivTransform.mli index 04e485869..f6a3f0da2 100644 --- a/src/phl/rules/equiv/ecEquivTransform.mli +++ b/src/phl/rules/equiv/ecEquivTransform.mli @@ -21,14 +21,23 @@ type equiv_transform = { (symmetrically for [`Right]; the other program and memory are unchanged), where [c'] may live in an extended memory (fresh program - variables), and the entry is given the program variables of [&1] read - by [Q]. Each obligation becomes a premise (first, in order): + variables), and the entry is given the goal's hypotheses and the + program variables of [&1] read by [Q]. Each obligation becomes a + premise (first, in order): - [OPrefixPost (hd, cond)]: forall &2, hoare [hd : P ==> cond] ([P] read as an assertion on [&1], the other memory [&2] being universally quantified); - [OLossless ks]: phoare [ks : true ==> true] = 1 - (in the memory [&1] of [c], the other memory not involved). + (in the memory [&1] of [c], the other memory not involved); + - [OExprEq (xs, e, e')]: forall &1, forall xs, e = e' + ([&1] over the memory type of [c'], the other memory not involved); + - [OLocalEquiv (xs, s, s', R, W, M)]: + forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}] + (left: the memory of [c], right: that of [c']), the frame [F] being + the conjunction of the top-level conjuncts of [P] that only mention + [&1] (not [&2]) and are independent from [M] + ([EcPlTransform.frame]). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [REquivTransform { etr_side; etr_tr = t }]. Checker: diff --git a/src/phl/rules/hoare/ecHoareTransform.ml b/src/phl/rules/hoare/ecHoareTransform.ml index 8d8f6e091..a40f279eb 100644 --- a/src/phl/rules/hoare/ecHoareTransform.ml +++ b/src/phl/rules/hoare/ecHoareTransform.ml @@ -28,6 +28,7 @@ let hoare_transform_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_trans let m = fst hs.hs_m in let po = hs_po hs in let ctxt = { + trc_hyps = hyps; trc_env = env; trc_me = hs.hs_m; trc_post = lazy (POE.fold @@ -42,7 +43,11 @@ let hoare_transform_subgoals (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_trans f_hoareS (snd hs.hs_m) (hs_pr hs) hd (update_hs_ss cond po) | OLossless ks -> f_bdHoareS (snd hs.hs_m) - { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } in + { m; inv = f_true } ks { m; inv = f_true } FHeq { m; inv = f_r1 } + | OExprEq o -> + f_expr_eq r.trr_me o + | OLocalEquiv o -> + f_local_equiv env hs.hs_m (snd r.trr_me) (Some (hs_pr hs).inv) o in List.map obligation r.trr_obl @ [f_hoareS (snd r.trr_me) (hs_pr hs) r.trr_s po] diff --git a/src/phl/rules/hoare/ecHoareTransform.mli b/src/phl/rules/hoare/ecHoareTransform.mli index 876a7a4af..46f6f003e 100644 --- a/src/phl/rules/hoare/ecHoareTransform.mli +++ b/src/phl/rules/hoare/ecHoareTransform.mli @@ -17,12 +17,20 @@ type hoare_transform = { hoare [c : P ==> Q | E] where [c'] may live in an extended memory (fresh program variables), - and the entry is given the program variables read by [Q | E]. Each - obligation becomes a premise (first, in order): + and the entry is given the goal's hypotheses and the program variables + read by [Q | E]. Each obligation becomes a premise (first, in order): - [OPrefixPost (hd, cond)]: hoare [hd : P ==> cond | E] (the exceptional postconditions [E] of the goal are kept); - [OLossless ks]: phoare [ks : true ==> true] = 1 - (in the memory of [c]). + (in the memory of [c]); + - [OExprEq (xs, e, e')]: forall &m, forall xs, e = e' + ([&m] the memory of [c'], named after the goal's); + - [OLocalEquiv (xs, s, s', R, W, M)]: + forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}] + (left: the memory of [c], right: that of [c']), the frame [F] being + the conjunction of the top-level conjuncts of [P] that only mention + the memory of [c] and are independent from [M] + ([EcPlTransform.frame]). Side condition: [t] applies to [c] (otherwise fails with its message). Node: [RHoareTransform { htr_tr = t }]. Checker: "hoare-transform" (it diff --git a/src/phl/rules/transforms/ecTrCircuitChange.ml b/src/phl/rules/transforms/ecTrCircuitChange.ml new file mode 100644 index 000000000..932c95568 --- /dev/null +++ b/src/phl/rules/transforms/ecTrCircuitChange.ml @@ -0,0 +1,108 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the circuit change, resolved: the position is a + normalized (possibly nested) code position, the fresh locals are bound + by the entry itself (deterministically), and the new statement is typed + in the memory they extend. *) +type tr_circuit_change = { + trcc_at : EcMatching.Position.nm_codepos; + trcc_len : int; + trcc_binds : ovariable list; + trcc_stmt : stmt; +} + +type EcPlTransform.transform += TrCircuitChange of tr_circuit_change + +(* -------------------------------------------------------------------- *) +let invalid fmt = Format.kasprintf (fun msg -> raise (InvalidTransform msg)) fmt + +(* -------------------------------------------------------------------- *) +(* Replace the fragment by the new statement, provided that the circuit + checker establishes that they agree on the variables to keep. *) +let circuit_change (p : tr_circuit_change) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + + let mem = + List.fold_left + (fun mem v -> fst (EcMemory.bind_fresh v mem)) + ctxt.trc_me p.trcc_binds in + + let s' = p.trcc_stmt in + + let zp = + try Zpr.zipper_of_nm_cpos p.trcc_at s + with EcMatching.Position.InvalidCPos -> invalid "invalid code position" in + + if not (0 <= p.trcc_len && p.trcc_len <= List.length zp.z_tail) then + invalid "cannot find %d consecutive instructions at given position" + p.trcc_len; + + let target, tl = EcUtils.List.takedrop p.trcc_len zp.z_tail in + + (* [keep] is the set of variables on which [target] and [s'] must + agree. Let [R] be the variables read by both [target] and [s']. + We take for [keep]: + - the variables read by the code that may run after the fragment + (for each enclosing [while], its guard and its whole body), + and by the postcondition; + - if the fragment is inside a loop, [R]. + Soundness: the original and the new programs are related by + "the states agree on [keep]" (they are equal before the first + run of the fragment). The code that may run after the fragment + only reads [keep], so preserves this relation. When reaching the + fragment in states [m1] (original) and [m2] (new), let [m] be + [m2] updated with the values of [m1] on [read(target) \ R]. + Then [m] agrees with [m1] on [read(target)] and on [keep] (as + [R] is included in [keep]), and with [m2] on [read(s')] and on + [keep]. As [target] and [s'] are deterministic, we get + [target(m1) =keep target(m) =keep s'(m) =keep s'(m2)], the middle + equality being the one established by the circuit checker. + Outside a loop, the fragment is run once, from [m1 = m2], and + [R] does not need to be kept. + The circuit checker only accepts assignments (no [raise]): the + fragments always terminate normally, and an exception raised + afterwards is observed through the exceptional postconditions, + whose variables are in [trc_post]. *) + let keep = + let zpr = ((zp.z_head, tl), zp.z_path) in + EcPV.zpr_pv `Read `After env EcPV.PV.empty zpr in + let keep = + if Zpr.in_loop zp.z_path then + EcPV.PV.union keep + (EcPV.PV.inter + (EcPV.is_read env target) + (EcPV.is_read env s'.s_node)) + else keep in + let keep = EcPV.PV.union keep (Lazy.force ctxt.trc_post) in + (* The variables that are neither read nor written by [target] and + [s'] are left unchanged by both and need not be compared. This + drops the global variables, which [target] and [s'] cannot access + (this is checked by the circuit checker). *) + let keep = + let ts = target @ s'.s_node in + EcPV.PV.inter keep + (EcPV.PV.union (EcPV.is_read env ts) (EcPV.is_write env ts)) in + let st = EcLowCircuits.create_state (EcEnv.gstate env) in + + let equiv = + try EcCircuits.instrs_equiv ctxt.trc_hyps ~keep mem st target s'.s_node + with e -> + invalid "circuit-equivalence checker error: %s" (Printexc.to_string e) + in + if not equiv then + invalid "statements are not circuit-equivalent"; + + { trr_me = mem; + trr_s = Zpr.zip { zp with z_tail = s'.s_node @ tl }; + trr_obl = []; } + +let () = + register (function + | TrCircuitChange p -> Some (circuit_change p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrCircuitChange.mli b/src/phl/rules/transforms/ecTrCircuitChange.mli new file mode 100644 index 000000000..58f6d06bf --- /dev/null +++ b/src/phl/rules/transforms/ecTrCircuitChange.mli @@ -0,0 +1,45 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_circuit_change = { + trcc_at : nm_codepos; (* position of the first replaced + instruction (resolved, possibly + nested) *) + trcc_len : int; (* number n of replaced instructions *) + trcc_binds : ovariable list; (* the fresh locals, as requested *) + trcc_stmt : stmt; (* the new statement [b'], typed in the + memory extended with them *) +} + +(* [TrCircuitChange { trcc_at = p; trcc_len = n; trcc_binds = vs; + trcc_stmt = b' }] — replaces the [n] instructions [b] at position [p] + (in the block of [p], possibly nested) by [b'], in the memory extended + with the fresh program variables [vs] (bound one by one with + [EcMemory.bind_fresh]: a variable is renamed apart when its name is + already bound; deterministic), provided that [b] and [b'] are + circuit-equivalent on the variables [K] to keep: + + c = C[b; tl] ~~> c' = C[b'; tl] + + [K] is the set of the variables read by the code that may run after + [b] ([tl], the instructions following each enclosing instruction, and, + for each enclosing loop, its guard and its whole body: [EcPV.zpr_pv + `Read `After]), by the postcondition (the context's [trc_post], for + hoare including the exceptional postconditions) and, when [b] is in a + loop, by both [b] and [b'], restricted to the variables read or written + by [b] or [b']. The check is [EcCircuits.instrs_equiv] (under the + context's [trc_hyps]): [b] and [b'] only contain assignments to local + variables (no call, sampling, conditional, loop or [raise]), only + access local variables, and end, from every state, in states agreeing + on [K]. No obligation. + + Fails with "invalid code position" when [p] is not a position of [c], + "cannot find n consecutive instructions at given position" when the + block has fewer than [n] instructions from [p], "circuit-equivalence + checker error: ..." when the checker fails, and "statements are not + circuit-equivalent" when it does not establish the equivalence. *) +type EcPlTransform.transform += TrCircuitChange of tr_circuit_change diff --git a/src/phl/rules/transforms/ecTrExprChange.ml b/src/phl/rules/transforms/ecTrExprChange.ml new file mode 100644 index 000000000..d63027e03 --- /dev/null +++ b/src/phl/rules/transforms/ecTrExprChange.ml @@ -0,0 +1,115 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcAst +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the expression change, resolved: the range is an integer + gap range of the (possibly nested) block at a normalized path, the + replacements typed expressions over local identifiers recorded with + them. *) +type tr_expr_change = { + trec_range : EcMatching.Position.nm_codegap_range option; + trec_exprs : (EcIdent.t list * expr) option list; +} + +type EcPlTransform.transform += TrExprChange of tr_expr_change + +(* -------------------------------------------------------------------- *) +let invalid () = raise (InvalidTransform "invalid expression change") + +(* -------------------------------------------------------------------- *) +let exprs ?(locals = []) f acc (is : instr list) = + List.fold_left_map (i_fold_map_expr ~locals f) acc is + +let rec locals_of_path (path : Zpr.ipath) = + match path with + | ZTop -> [] + | ZWhile (_, (_, path)) + | ZIfThen (_, (_, path), _) + | ZIfElse (_, _, (_, path)) -> locals_of_path path + | ZMatch (_, (_, path), ctxt) -> locals_of_path path @ ctxt.locals + +(* -------------------------------------------------------------------- *) +(* [rename xs ys e]: [e] with the locals [xs] simultaneously renamed to + [ys] (taken with the types of [xs]). *) +let rename (xs : (EcIdent.t * ty) list) (ys : EcIdent.t list) (e : expr) = + let subst = + List.fold_left2 + (fun subst (x, ty) y -> + EcCoreSubst.bind_elocal subst x (EcTypes.e_local y ty)) + EcCoreSubst.Fsubst.f_subst_id xs ys + in EcCoreSubst.e_subst subst e + +(* Replace [e] (with the match-arm locals [xs] in scope) as told by the + next element of the replacements, accumulating its obligation. The + side conditions ensure that [forall ys, e[xs := ys] = e'] implies that + [e] and [e'[ys := xs]] agree for every value of [xs]: the renamings + capture nothing. *) +let change xs (obls, cs) (e : expr) = + match cs with + | [] -> invalid () + + | None :: cs -> + (obls, cs), e + + | Some (ys, e') :: cs -> + if not (EcTypes.ty_equal e.e_ty e'.e_ty) then invalid (); + if List.length ys <> List.length xs then invalid (); + + let sxs = EcIdent.Sid.of_list (List.fst xs) in + let sys = EcIdent.Sid.of_list ys in + + if EcIdent.Sid.cardinal sys <> List.length ys then invalid (); + + if EcIdent.Mid.exists + (fun x _ -> EcIdent.Sid.mem x sys && not (EcIdent.Sid.mem x sxs)) + (EcTypes.e_fv e) then invalid (); + + if EcIdent.Mid.exists + (fun x _ -> EcIdent.Sid.mem x sxs && not (EcIdent.Sid.mem x sys)) + (EcTypes.e_fv e') then invalid (); + + let lhs = rename xs ys e in + let lcs = List.map2 (fun y (_, ty) -> (y, ty)) ys xs in + let obl = OExprEq { oee_locals = lcs; oee_lhs = lhs; oee_rhs = e'; } in + + (obl :: obls, cs), rename lcs (List.fst xs) e' + +(* -------------------------------------------------------------------- *) +(* Replace the expressions of the range (of the whole statement), in + program order, one obligation per replaced expression. *) +let expr_change (p : tr_expr_change) (ctxt : tr_ctxt) (s : stmt) = + let (obls, cs), s = + match p.trec_range with + | None -> + let acc, is = exprs change ([], p.trec_exprs) s.s_node in + acc, stmt is + + | Some (path, (start, fin)) -> + let invalid_cpos () = + raise (InvalidTransform "invalid code position") in + let zpr = + try Zpr.zipper_of_nm_cpos (path, start) s + with EcMatching.Position.InvalidCPos -> invalid_cpos () in + if not (start <= fin && fin - start <= List.length zpr.z_tail) then + invalid_cpos (); + let body, epilog = List.takedrop (fin - start) zpr.z_tail in + let locals = locals_of_path zpr.z_path in + let acc, body = exprs ~locals change ([], p.trec_exprs) body in + acc, Zpr.zip { zpr with z_tail = body @ epilog } + in + + if not (List.is_empty cs) then invalid (); + + { trr_me = ctxt.trc_me; + trr_s = s; + trr_obl = List.rev obls; } + +let () = + register (function + | TrExprChange p -> Some (expr_change p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrExprChange.mli b/src/phl/rules/transforms/ecTrExprChange.mli new file mode 100644 index 000000000..5d4cf3b8f --- /dev/null +++ b/src/phl/rules/transforms/ecTrExprChange.mli @@ -0,0 +1,65 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +(* The expressions of the range, in program order (see [exprs]): each one + is either unchanged ([None]) or replaced ([Some (ys, e')]), [e'] being + stated over the local identifiers [ys], one per match-arm local in + scope of the expression (in the order of [exprs]). *) +type tr_expr_change = { + trec_range : nm_codegap_range option; (* the range [p : [s..f)] + (resolved, possibly nested); + [None]: the whole statement *) + trec_exprs : (EcIdent.t list * expr) option list; + (* the replacements, in program + order *) +} + +(* [TrExprChange { trec_range = r; trec_exprs = cs }] — replaces + expressions of the instructions of the range [r] (of the whole + statement when [r] is [None]), at any depth (guards and bodies of + [if] / [while], discriminants and arms of [match]): + + c = C[b] ~~> c' = C[b'] (b' is b with e_i replaced by e_i') + + The expressions of [b] are enumerated in program order ([exprs]), each + with the match-arm locals [xs_i] in scope at its occurrence (those of + the enclosing arms of [r] first). The list [cs] has one element per + expression: [None] leaves [e_i] unchanged; [Some (ys_i, e_i')] replaces + [e_i] by [e_i'[ys_i := xs_i]]. One obligation per replaced expression, + in program order: + + OExprEq { oee_locals = ys_i : tys_i; oee_lhs = e_i[xs_i := ys_i]; + oee_rhs = e_i' } + + i.e. [forall &m, forall ys_i, e_i[xs_i := ys_i] = e_i'], [tys_i] being + the types of [xs_i]. Same memory. + + Side conditions, for each replaced [e_i]: [e_i'] has the type of [e_i]; + [ys_i] has the length of [xs_i]; the [ys_i] are pairwise distinct and + none of them is free in [e_i] other than as one of the [xs_i]; no local + of [xs_i] that is not in [ys_i] is free in [e_i'] (so that the + renamings capture nothing). Fails with "invalid code position" when [r] + is not a range of [c], and with "invalid expression change" when [cs] + does not have one element per expression or a side condition does not + hold. *) +type EcPlTransform.transform += TrExprChange of tr_expr_change + +(* ==================================================================== *) +(* Enumeration (shared with the derived tactic) *) + +(* [exprs] is the enumeration of the entry: [exprs f acc s] folds [f + locals] over the expressions of [s] in program order, [locals] being + the match-arm locals in scope (on top of [?locals]), mapping each + expression to the result of [f]. *) +val exprs : + ?locals:(EcIdent.t * ty) list + -> ((EcIdent.t * ty) list -> 'a -> expr -> 'a * expr) + -> 'a -> instr list -> 'a * instr list + +(* [locals_of_path p]: the match-arm locals in scope at the zipper path + [p], outermost first. *) +val locals_of_path : EcMatching.Zipper.ipath -> (EcIdent.t * ty) list diff --git a/src/phl/rules/transforms/ecTrIdAssign.ml b/src/phl/rules/transforms/ecTrIdAssign.ml new file mode 100644 index 000000000..b1a5cfae5 --- /dev/null +++ b/src/phl/rules/transforms/ecTrIdAssign.ml @@ -0,0 +1,49 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcModules +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the identity assignment, resolved: the position is a + normalized (possibly nested) code position, the variable a typed + program variable. *) +type tr_idassign = { + tria_at : EcMatching.Position.nm_codepos; + tria_pv : prog_var * ty; +} + +type EcPlTransform.transform += TrIdAssign of tr_idassign + +(* -------------------------------------------------------------------- *) +(* Insert [x <- x], [x] being a variable of the memory when local. *) +let idassign (p : tr_idassign) (ctxt : tr_ctxt) (s : stmt) = + let (pv, ty) = p.tria_pv in + + begin match pv with + | PVloc x -> + let bound = + match EcMemory.lookup_me x ctxt.trc_me with + | Some (v, _, _) -> ty_equal v.v_type ty + | None -> false in + if not bound then + raise (InvalidTransform "invalid program variable") + | PVglob _ -> () + end; + + let zpr = + try Zpr.zipper_of_nm_cpos p.tria_at s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid code position") in + + let i = i_asgn (LvVar (pv, ty), e_var pv ty) in + + { trr_me = ctxt.trc_me; + trr_s = Zpr.zip { zpr with Zpr.z_tail = i :: zpr.Zpr.z_tail; }; + trr_obl = []; } + +let () = + register (function + | TrIdAssign p -> Some (idassign p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrIdAssign.mli b/src/phl/rules/transforms/ecTrIdAssign.mli new file mode 100644 index 000000000..8237c0d6b --- /dev/null +++ b/src/phl/rules/transforms/ecTrIdAssign.mli @@ -0,0 +1,23 @@ +(* -------------------------------------------------------------------- *) +open EcTypes +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_idassign = { + tria_at : nm_codepos; (* insertion position (resolved, possibly + nested; may be the end of its block) *) + tria_pv : prog_var * ty; (* the program variable [x], typed *) +} + +(* [TrIdAssign { tria_at = p; tria_pv = x : t }] — inserts, at position + [p], the identity assignment of [x]: + + c = C[tl] ~~> c' = C[x <- x; tl] + + No obligation, same memory. Side condition: when [x] is a local + variable, it is bound in the memory, with type [t]. Fails with + "invalid code position" when [p] is not a position of [c], and + "invalid program variable" when the side condition does not hold. *) +type EcPlTransform.transform += TrIdAssign of tr_idassign diff --git a/src/phl/rules/transforms/ecTrStmtChange.ml b/src/phl/rules/transforms/ecTrStmtChange.ml new file mode 100644 index 000000000..2463b3aec --- /dev/null +++ b/src/phl/rules/transforms/ecTrStmtChange.ml @@ -0,0 +1,99 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcModules +open EcPV +open EcPlTransform + +module Zpr = EcMatching.Zipper + +(* -------------------------------------------------------------------- *) +(* Parameters of the statement change, resolved: the range is an integer + gap range of the (possibly nested) block at a normalized path, the + fresh locals are bound by the entry itself (deterministically), and the + new statement is typed in the memory they extend. *) +type tr_stmt_change = { + trsc_range : EcMatching.Position.nm_codegap_range; + trsc_binds : ovariable list; + trsc_stmt : stmt; +} + +type EcPlTransform.transform += TrStmtChange of tr_stmt_change + +(* -------------------------------------------------------------------- *) +(* Replace the range by the new statement, under a local equivalence + between the two fragments. *) +let stmt_change (p : tr_stmt_change) (ctxt : tr_ctxt) (s : stmt) = + let env = ctxt.trc_env in + let (path, (start, fin)), s' = p.trsc_range, p.trsc_stmt in + + let invalid_cpos () = raise (InvalidTransform "invalid code position") in + + let zpr = + try Zpr.zipper_of_nm_cpos (path, start) s + with EcMatching.Position.InvalidCPos -> invalid_cpos () in + if not (start <= fin && fin - start <= List.length zpr.z_tail) then + invalid_cpos (); + let b, epilog = EcUtils.List.takedrop (fin - start) zpr.z_tail in + + let me, _ = EcMemory.bindall_fresh p.trsc_binds ctxt.trc_me in + + (* The code around the fragment: [zpr] without the fragment. *) + let around = (zpr.z_head, epilog), zpr.z_path in + + (* Inside a loop, the fragment may run several times. Its later runs + start after the surrounding code of the loop, but also after the + previous runs of the fragment itself, and from states where the two + programs only agree on the observable variables (see [obs] below). *) + let inloop = Zpr.in_loop zpr.z_path in + + (* Collect the variables that may be modified before (a run of) the + fragment: by the surrounding context and, inside a loop, by the + previous runs of the original fragment. The frame of the local + equivalence (computed by the rule from its precondition) only keeps + what is independent from them. *) + let modi = + let modi = zpr_pv `Write `Before env PV.empty around in + if inloop then is_write_r env modi b else modi in + + (* The variables read by both fragments, assumed equal by the local + equivalence. *) + let reads = PV.inter (is_read env b) (is_read env s'.s_node) in + + (* The observable variables: those read by the code that may run after + the fragment (for an enclosing loop, its guard and its whole body) + and by the postcondition. Inside a loop, we add the variables read + by both fragments, i.e. the ones assumed equal by the local + equivalence below. + Soundness: the original and new programs are related by "the states + agree on [obs]" (they are equal before the first run of the + fragment). The code after the fragment only reads [obs], so it + preserves this relation. When reaching the fragment, the relation + implies the equalities of the precondition of the local + equivalence (their variables are in [obs] when in a loop), the + frame holds on the original side as no code run so far writes its + variables (see [modi]), and the local equivalence then + re-establishes the relation: the observable variables that are + written are equal, and the other ones are unchanged. *) + let obs = + let obs = zpr_pv `Read `After env PV.empty around in + let obs = if inloop then PV.union obs reads else obs in + PV.union obs (Lazy.force ctxt.trc_post) in + + let written = + let written = is_write_r env PV.empty b in + let written = is_write_r env written s'.s_node in + PV.inter written obs in + + { trr_me = me; + trr_s = Zpr.zip { zpr with z_tail = s'.s_node @ epilog }; + trr_obl = [OLocalEquiv { ole_locals = EcTrExprChange.locals_of_path zpr.z_path; + ole_orig = stmt b; + ole_new = s'; + ole_reads = reads; + ole_writes = written; + ole_modi = modi; }]; } + +let () = + register (function + | TrStmtChange p -> Some (stmt_change p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrStmtChange.mli b/src/phl/rules/transforms/ecTrStmtChange.mli new file mode 100644 index 000000000..f945918e0 --- /dev/null +++ b/src/phl/rules/transforms/ecTrStmtChange.mli @@ -0,0 +1,54 @@ +(* -------------------------------------------------------------------- *) +open EcAst +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_stmt_change = { + trsc_range : nm_codegap_range; (* the range [p : [s..f)] to replace + (resolved, possibly nested) *) + trsc_binds : ovariable list; (* the fresh locals, as requested *) + trsc_stmt : stmt; (* the new statement [b'], typed in the + memory extended with them *) +} + +(* [TrStmtChange { trsc_range = r; trsc_binds = vs; trsc_stmt = b' }] — + replaces the instructions [b] of the range [r] (of a possibly nested + block) by [b'], in the memory extended with the fresh program variables + [vs] ([EcMemory.bindall_fresh vs]: a variable is renamed apart when its + name is already bound; deterministic, so that the statement typed by + the tactic in that memory and the checker agree): + + c = C[b] ~~> c' = C[b'] + + with [Before] / [After] the code other than [b] that may run before / + after [b] ([EcPV.zpr_pv]: the instructions around [b] in its block and + the enclosing ones, and for each enclosing loop, its guard and its + whole body): + - [M]: the variables written [Before] [b], and, when [b] is in a loop, + by [b] itself (its previous runs); + - [R]: the variables read by both [b] and [b']; + - [O]: the variables read [After] [b], by the postcondition (the + context's [trc_post]: for hoare including the exceptional + postconditions, for phoare not the bound, evaluated in the initial + memory), and, when [b] is in a loop, [R]; + - [W]: the variables written by [b] or [b'] that are in [O]. + One obligation, [OLocalEquiv { ole_locals = xs; ole_orig = b; + ole_new = b'; ole_reads = R; ole_writes = W; ole_modi = M }], [xs] + being the match-arm locals in scope at [b] (which [b] may mention: + the local equivalence holds for all their values). + + Soundness: the original and new programs are related by "the states + agree on [O]" (they are equal before the first run of [b]). The code + after [b] only reads [O], so it preserves this relation. When reaching + [b], the relation implies [={R}] ([R] is in [O] in a loop; outside, + [b] runs once, from equal states), the frame holds on the original + side as no code run so far writes its variables ([M]), and the local + equivalence re-establishes the relation: the observable variables that + are written are equal, and the other ones are unchanged. The fresh + variables are read by no code but [b'], and are not constrained by + the local equivalence. + + Fails with "invalid code position" when [r] is not a range of [c]. *) +type EcPlTransform.transform += TrStmtChange of tr_stmt_change diff --git a/tests/rewrite-transform.ec b/tests/rewrite-transform.ec new file mode 100644 index 000000000..b5247de50 --- /dev/null +++ b/tests/rewrite-transform.ec @@ -0,0 +1,354 @@ +(* `proc rewrite`, `proc rewrite /=`, `proc change`, `proc change circuit` + and `idassign` as program transformations: in every logic where they + exist (hoare, ehoare, phoare, equiv on both sides; `proc change + circuit` and `idassign` are hoare only), at top-level and nested + positions (in the branches of an `if`, the body of a `while`, the arms + of a `match`, with the arm locals in scope), with fresh locals, and + their error paths. Each tactic is a separate sentence, so that the + goals it leaves can be compared across builds. *) +require import AllCore List Distr Xreal QFABV. + +op foo : int -> int. +axiom fooE (x : int) : foo x = x + 1. + +hint simplify fooE. + +type t = [A | B of int]. + +exception oops. + +module M = { + var g : int + + proc f(a : int, b : bool, o : t) : int = { + var x, y, z : int; + x <- a + 0; + y <- foo x; + if (b) { + z <- y + 0; + } else { + z <- foo 0; + } + match o with + | A => { x <- 0 + 2; } + | B v => { x <- v + 0; z <- foo v; } + end; + while (x < 10) { + x <- x + 0; + y <- foo y; + } + return x + y + z; + } + + proc e(a : int) : int = { + var x : int; + x <- a; + if (x = 0) { raise oops; } + return x; + } +}. + +(* ==================================================================== *) +(* proc rewrite *) + +lemma hoare_rw : hoare [M.f : true ==> 0 <= res]. +proof. +proc. +proc rewrite 1 addz0. +proc rewrite 3.1 addz0. +proc rewrite 4#B.1 addz0. +proc rewrite 4#A.1 addzC. +proc rewrite 5.:[1..2] addz0. +proc rewrite 5 ltzE. +admit. +qed. + +lemma hoare_rw_simpl : hoare [M.f : true ==> 0 <= res]. +proof. +proc. +proc rewrite [1..2] /=. +proc rewrite 4#B.:[1..2] /=. +proc rewrite /=. +proc rewrite /=. +admit. +qed. + +lemma ehoare_rw : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +proc rewrite 1 addz0. +proc rewrite 3?1 /=. +proc rewrite 4#B.1 addz0. +proc rewrite /=. +admit. +qed. + +lemma phoare_rw : phoare [M.f : true ==> 0 <= res] = 1%r. +proof. +proc. +proc rewrite 1 addz0. +proc rewrite 3.1 addz0. +proc rewrite 4#B.2 /=. +proc rewrite 5.1 addz0. +admit. +qed. + +lemma equiv_rw : equiv [M.f ~ M.f : ={arg} ==> ={res}]. +proof. +proc. +proc rewrite {1} 1 addz0. +proc rewrite {2} 3.1 addz0. +proc rewrite {1} 4#B.1 addz0. +proc rewrite {2} 4#B.:[1..2] /=. +proc rewrite {1} /=. +proc rewrite {2} 5.:[1..2] /=. +admit. +qed. + +lemma rw_errors : hoare [M.f : true ==> 0 <= res]. +proof. +proc. +fail proc rewrite 2 addz0. (* no occurrence *) +fail proc rewrite 12 addz0. (* invalid code position *) +fail proc rewrite {1} 1 addz0. (* side for a non-relational goal *) +fail proc rewrite 1 fooE. (* no occurrence *) +fail proc rewrite 1 foo. (* not a lemma *) +admit. +qed. + +lemma rw_errors_equiv : equiv [M.f ~ M.f : ={arg} ==> ={res}]. +proof. +proc. +fail proc rewrite 1 addz0. (* no side for a relational goal *) +fail proc rewrite {1} 2 addz0. (* no occurrence *) +admit. +qed. + +lemma rw_errors_fun : hoare [M.f : true ==> 0 <= res]. +proof. +fail proc rewrite 1 addz0. (* not a statement judgement *) +admit. +qed. + +(* ==================================================================== *) +(* proc change *) + +lemma hoare_change : hoare [M.f : 0 <= a ==> 0 <= res]. +proof. +proc. +proc change 1 : { x <- a; }. +admit. +proc change 3.1 : { z <- y; }. +admit. +proc change 4#B.:[1..2] : [w : int] { w <- y; x <- w; z <- w + 1; }. +admit. +proc change 5.1 : { x <- x; }. +admit. +proc change <2 : { M.g <- 0; }. +admit. +proc change [6..6] : { while (x < 10) { x <- x + 0; y <- y + 1; } }. +admit. +admit. +qed. + +lemma ehoare_change : ehoare [M.f : 1%xr ==> 1%xr]. +proof. +proc. +proc change 1 : { x <- a; }. +admit. +proc change 3?1 : [w : int] { w <- 0; z <- w + 1; }. +admit. +proc change 5.2 : { y <- y + 1; }. +admit. +admit. +qed. + +lemma phoare_change : phoare [M.f : 0 <= a ==> 0 <= res] = 1%r. +proof. +proc. +proc change 1 : { x <- a; }. +admit. +proc change 3.1 : [w : int] { w <- y; z <- w; }. +admit. +proc change 4#B.2 : { z <- x + 1; }. +admit. +proc change 5.:[1..2] : { y <- foo y; x <- x + 0; }. +admit. +admit. +qed. + +lemma equiv_change : equiv [M.f ~ M.f : ={arg} /\ 0 <= a{1} /\ a{2} < 5 ==> ={res}]. +proof. +proc. +proc change {1} 1 : { x <- a; }. +admit. +proc change {2} 1 : [w : int] { w <- a; x <- w; }. +admit. +proc change {1} 3.1 : { z <- y; }. +admit. +proc change {2} 5#B.:[1..2] : { x <- y; z <- y + 1; }. +admit. +proc change {1} 5.1 : { x <- x; }. +admit. +proc change {2} >(-1) : { y <- y; }. +admit. +admit. +qed. + +(* ehoare: the frame is taken from the boolean part [P] of a + precondition [P `|` f] (the reference build took the whole real-valued + precondition as a conjunct of the precondition of the local + equivalence, which was then ill-typed). *) +lemma ehoare_change_frame : ehoare [M.f : (0 <= a) `|` 1%xr ==> 1%xr]. +proof. +proc. +proc change 1 : { x <- a; }. +admit. +proc change 2 : { y <- x + 1; }. +admit. +admit. +qed. + +lemma change_errors : hoare [M.f : true ==> 0 <= res]. +proof. +proc. +fail proc change 12 : { x <- a; }. (* invalid code position *) +fail proc change {1} 1 : { x <- a; }. (* side for a non-relational goal *) +fail proc change 1 : { x <- w; }. (* unknown variable *) +admit. +qed. + +lemma change_errors_equiv : equiv [M.f ~ M.f : ={arg} ==> ={res}]. +proof. +proc. +fail proc change 1 : { x <- a; }. (* no side *) +admit. +qed. + +lemma change_errors_fun : hoare [M.f : true ==> 0 <= res]. +proof. +fail proc change 1 : { x <- a; }. (* not inlined *) +admit. +qed. + +(* An exceptional postcondition reading a variable written by the + fragment: the variable is observable. *) +lemma hoare_change_exn : hoare [M.e : true ==> true | oops => M.g = 0]. +proof. +proc. +proc change 1 : { x <- a; M.g <- x; }. +admit. +admit. +qed. + +(* ==================================================================== *) +(* proc change circuit / idassign (hoare only) *) + +type W8. + +op to_bits : W8 -> bool list. +op from_bits : bool list -> W8. +op of_int : int -> W8. +op to_uint : W8 -> int. +op to_sint : W8 -> int. + +bind bitstring to_bits from_bits to_uint to_sint of_int W8 8. +realize gt0_size by admit. +realize tolistP by admit. +realize oflistP by admit. +realize touintP by admit. +realize tosintP by admit. +realize ofintP by admit. +realize size_tolist by admit. + +op (+^) : W8 -> W8 -> W8. +bind op W8 (+^) "xor". +realize bvxorP by admit. + +module C = { + var gw : W8 + + proc f (a : W8, b : W8, c0 : bool) = { + var c, d : W8; + c <- a +^ b; + if (c0) { + d <- b +^ a; + c <- d +^ c; + } + return c; + } + + proc g (a : W8, b : W8) = { + var c : W8; + c <- a +^ b; + gw <- c; + return c; + } + + proc r (a : W8, b : W8) = { + var c : W8; + c <$ dunit a; + return c; + } +}. + +lemma hoare_circuit (a_ b_ : W8) : + hoare[C.f : a_ = a /\ b_ = b ==> true]. +proof. +proc. +proc change circuit 1 + 1 { c <- b +^ a; }. +proc change circuit 2.1 + 2 { d <- a +^ b; c <- d +^ c; }. +proc change circuit [e : W8] 2.1 + 1 { e <- b; d <- a +^ e; }. +idassign 1 c. +idassign 3.2 d. +idassign 4 C.gw. +admit. +qed. + +lemma circuit_errors (a_ b_ : W8) : + hoare[C.f : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. +proc. +fail proc change circuit 1 + 1 { c <- a; }. (* not equivalent *) +fail proc change circuit 1 + 3 { c <- b +^ a; }. (* too many instructions *) +fail proc change circuit 12 + 1 { c <- b +^ a; }. (* invalid position *) +fail proc change circuit 1 + 1 { c <- e; }. (* unknown variable *) +fail proc change circuit 1 + 1 { C.gw <- a; c <- b +^ a; }. (* global *) +fail proc change circuit [_ : W8] 1 + 1 { c <- b +^ a; }. (* no name *) +fail idassign 1 e. (* unknown variable *) +fail idassign 12 c. (* invalid position *) +admit. +qed. + +lemma circuit_errors_global (a_ b_ : W8) : + hoare[C.g : a_ = a /\ b_ = b ==> res = a_ +^ b_]. +proof. +proc. +fail proc change circuit 1 + 2 { c <- b +^ a; C.gw <- c; }. (* checker error *) +admit. +qed. + +lemma circuit_errors_rnd (a_ b_ : W8) : + hoare[C.r : a_ = a /\ b_ = b ==> true]. +proof. +proc. +fail proc change circuit 1 + 1 { c <- a; }. (* checker error *) +admit. +qed. + +lemma circuit_errors_exn (a_ b_ : W8) : + hoare[C.f : a_ = a /\ b_ = b ==> true | oops => true]. +proof. +proc. +fail proc change circuit 1 + 1 { c <- b +^ a; }. (* exceptions *) +admit. +qed. + +lemma circuit_errors_logic (a_ b_ : W8) : + equiv[C.f ~ C.f : ={arg} ==> ={res}]. +proof. +proc. +fail proc change circuit 1 + 1 { c <- b +^ a; }. (* hoare only *) +fail idassign 1 c. (* hoare only *) +admit. +qed.