From e70addb3591f84a147416bc5ef88892c81a16800 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Thu, 8 Oct 2026 08:45:38 +0200 Subject: [PATCH] refactor(pl): proc rewrite / change as program transformations PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates `proc rewrite` (and `proc rewrite /=`), `proc change`, `proc change circuit` and `idassign` onto the program transformations (one trusted transformation rule per logic + a catalogue of entries): - four catalogue entries in src/phl/rules/transforms/: EcTrExprChange (replaces expressions of a possibly nested range, or of the whole statement, in program order; each replacement is stated over recorded identifiers for the match-arm locals in scope, with type and capture side conditions), EcTrStmtChange (replaces a range by a statement over fresh locals, bound by the entry with EcMemory.bindall_fresh; the modified, observable and shared-read variables are computed by the entry, loop case included), EcTrCircuitChange (the circuit-equivalence check and its keep-set are run by the entry, under the goal's hypotheses) and EcTrIdAssign (inserts x <- x); - two new obligation kinds in EcPlTransform, with their premise in each of the four transformation rules: OExprEq forall &m, forall xs, e = e' and OLocalEquiv forall xs, equiv [s ~ s' : ={R} /\ F{1} ==> ={W}] (xs the match-arm locals in scope), whose frame F is computed by each rule from its own precondition (shared helper EcPlTransform.frame; for ehoare, the boolean part P of a precondition P `|` f, and no frame otherwise); - the transformation context gets the goal's hypotheses (trc_hyps), needed by the circuit checker; - EcPhlRewrite and EcPhlRwPrgm reduced to derived tactics: they resolve their arguments, keep their checks and messages, and apply the transformation rule of the goal's logic (rw_prgm: hoare only); `proc rewrite` still discharges its equalities on the spot; interfaces unchanged; `proc rewrite pre` untouched (conseq). Behaviour is preserved (goals and messages compared with the reference build on the new test and on the existing tests, including the ehoare frame and the quantification over match-arm locals fixed on main), except for phoare `proc change`: the variables read by the bound are no longer observable (the bound is evaluated in the initial memory), so the postcondition of the local equivalence may have fewer equalities. Validation: new test tests/rewrite-transform.ec (every tactic in every logic where it exists, both equiv sides, nested positions with match-arm locals, fresh locals, error paths); stdlib, unit and examples under EC_RECHECK=1, zero RecheckFailure. Each new premise (OExprEq, OLocalEquiv, in each of the four rules) and each new entry, when broken in the checker only, is caught only under EC_RECHECK (files caught on stdlib / unit / examples: equiv OExprEq 1/4/0, hoare OExprEq 0/4/0, ehoare and bdhoare OExprEq 0/1/0, hoare and equiv OLocalEquiv 0/2/0, ehoare and bdhoare OLocalEquiv 0/1/0, expr-change 1/5/0, stmt-change 0/2/0, circuit-change 0/3/0, idassign 0/1/0). --- src/phl/README.md | 15 +- src/phl/REFACTORING.md | 60 ++- src/phl/ecPhlRewrite.ml | 273 ++++---------- src/phl/ecPhlRwPrgm.ml | 104 ++--- src/phl/rules/bdhoare/ecBdHoareTransform.ml | 7 +- src/phl/rules/bdhoare/ecBdHoareTransform.mli | 16 +- src/phl/rules/ecPlTransform.ml | 70 ++++ src/phl/rules/ecPlTransform.mli | 72 +++- src/phl/rules/ehoare/ecEHoareTransform.ml | 27 +- src/phl/rules/ehoare/ecEHoareTransform.mli | 15 +- src/phl/rules/equiv/ecEquivTransform.ml | 7 +- src/phl/rules/equiv/ecEquivTransform.mli | 15 +- src/phl/rules/hoare/ecHoareTransform.ml | 7 +- src/phl/rules/hoare/ecHoareTransform.mli | 14 +- src/phl/rules/transforms/ecTrCircuitChange.ml | 108 ++++++ .../rules/transforms/ecTrCircuitChange.mli | 45 +++ src/phl/rules/transforms/ecTrExprChange.ml | 115 ++++++ src/phl/rules/transforms/ecTrExprChange.mli | 65 ++++ src/phl/rules/transforms/ecTrIdAssign.ml | 49 +++ src/phl/rules/transforms/ecTrIdAssign.mli | 23 ++ src/phl/rules/transforms/ecTrStmtChange.ml | 99 +++++ src/phl/rules/transforms/ecTrStmtChange.mli | 54 +++ tests/rewrite-transform.ec | 354 ++++++++++++++++++ 23 files changed, 1305 insertions(+), 309 deletions(-) create mode 100644 src/phl/rules/transforms/ecTrCircuitChange.ml create mode 100644 src/phl/rules/transforms/ecTrCircuitChange.mli create mode 100644 src/phl/rules/transforms/ecTrExprChange.ml create mode 100644 src/phl/rules/transforms/ecTrExprChange.mli create mode 100644 src/phl/rules/transforms/ecTrIdAssign.ml create mode 100644 src/phl/rules/transforms/ecTrIdAssign.mli create mode 100644 src/phl/rules/transforms/ecTrStmtChange.ml create mode 100644 src/phl/rules/transforms/ecTrStmtChange.mli create mode 100644 tests/rewrite-transform.ec 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.