From 4b74ba8694191bfe92da65df596832d6aab18cf5 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Wed, 7 Oct 2026 10:53:51 +0200 Subject: [PATCH] refactor(pl): rcond and rmatch as program transformations PR of the program-logic reorganization stack (see src/phl/REFACTORING.md). It migrates the `rcond` / `rmatch` tactic class (rcondt, rcondf, match C k) onto the transformation rule of each logic: - rules/transforms/ecTrRCond.ml, ecTrRMatch.ml: two catalogue entries, with resolved parameters. `rcond` (instruction index, branch) decides the if / while at that index, with the obligation `OPrefixPost (hd, b)` (resp. `!b`). `rmatch` (instruction index, constructor index) decides the match, the arguments of the constructor being assigned to fresh program variables (`ys <- oget (get_as_C e)`), with the obligation `OPrefixPost (hd, exists xs, e = C xs)`: the unframed form of `match C k`. - rules/ecPlRCond.ml: the decisions shared by the entries, the framed rules and the tactics (the instruction at a resolved index, the rmatch decomposition and framing condition, and the tactic-side resolution with today's error messages). - rules/{hoare,ehoare,bdhoare,equiv}/ecRMatch.ml: the framed form of `match C k` (used when the variables of `e` are neither read nor written by the prefix, and the judgement is hoare, ehoare or phoare `<=`, or the prefix is empty) adds `e = C ys` to the precondition: it is not a program transformation, so it stays a separate trusted rule per logic, `t__rmatch_framed`, kept over the whole statement (implicit seq) pending a later discussion. Its node records the resolved indices, its pure builder re-checks every side condition (a match, a valid constructor, `e` independent of the prefix, the per-logic termination condition), and its checker is "-rmatch-framed". The .mli states it as an inference rule and why it is only sound under that condition. - The tactics are derived in every logic (EcRCond, EcRMatch): resolve the position and the constructor, check what they always checked, then apply `t__transform` with the entry (equiv: on the given side), or the framed rule when today's condition selects the framed form. The `t_low*` wrappers are gone. - EcPhlRCond is reduced to the dispatchers and positional adapters; its interface is unchanged, so `if`, `match` and `unroll for` keep using it (`if` now goes through the transformation rule, `match` through the framed rule). - REFACTORING.md, README.md, EcPlTransform: the catalogue now lists rcond and rmatch, and names the framed-match rule. Behaviour is preserved: on every rcond / match step of the new test and of tests/rmatch-frame.ec, tests/rmatch-ehoare.ec and tests/single_match.ec, the goals printed by the reference and new builds are identical, and so is every error message, except for one alpha-renaming: the prefix obligation of the unframed equiv `match C {i} k` (non-empty prefix) is now stated as the transformation rule states it for `rcond`, quantifying over `&m` (was the name of the other memory, e.g. `&2`) with the hoare memory `&hr` (was `&1`). The premises keep their order (obligation first). A new test, tests/rcond.ec, exercises rcondt / rcondf on if and while in every logic (both equiv sides, hoare exceptions kept), framed and unframed match C k (hoare, ehoare, phoare `<=`, phoare `=` forcing the unframed form, equiv with a non-empty prefix, empty prefix framed), the plain match, and the error paths; it passes with the reference build too. The stdlib (128 files), the unit tests (124) and the examples (49) pass under EC_RECHECK=1 with no RecheckFailure. Each checker, when deliberately broken, is caught only under EC_RECHECK: on the new test, and on the stdlib through rcond / if for hoare-transform (8 files), bdhoare-transform (13) and equiv-transform (21). ehoare-transform and the four rmatch-framed checkers are not used by the stdlib; they are caught on the unit tests (2 files for ehoare-transform and ehoare-rmatch-framed, 3 for the hoare, bdhoare and equiv rmatch-framed checkers). --- src/ecTyping.ml | 2 +- src/phl/README.md | 12 +- src/phl/REFACTORING.md | 42 ++- src/phl/ecPhlRCond.ml | 373 +++------------------ src/phl/rules/bdhoare/ecBdHoareRCond.ml | 28 ++ src/phl/rules/bdhoare/ecBdHoareRCond.mli | 35 ++ src/phl/rules/bdhoare/ecBdHoareRMatch.ml | 92 +++++ src/phl/rules/bdhoare/ecBdHoareRMatch.mli | 77 +++++ src/phl/rules/ecPlRCond.ml | 157 +++++++++ src/phl/rules/ecPlRCond.mli | 76 +++++ src/phl/rules/ecPlTransform.mli | 6 +- src/phl/rules/ehoare/ecEHoareRCond.ml | 30 ++ src/phl/rules/ehoare/ecEHoareRCond.mli | 37 ++ src/phl/rules/ehoare/ecEHoareRMatch.ml | 94 ++++++ src/phl/rules/ehoare/ecEHoareRMatch.mli | 78 +++++ src/phl/rules/ehoare/ecEHoareTransform.mli | 3 - src/phl/rules/equiv/ecEquivRCond.ml | 35 ++ src/phl/rules/equiv/ecEquivRCond.mli | 37 ++ src/phl/rules/equiv/ecEquivRMatch.ml | 115 +++++++ src/phl/rules/equiv/ecEquivRMatch.mli | 78 +++++ src/phl/rules/hoare/ecHoareRCond.ml | 28 ++ src/phl/rules/hoare/ecHoareRCond.mli | 35 ++ src/phl/rules/hoare/ecHoareRMatch.ml | 88 +++++ src/phl/rules/hoare/ecHoareRMatch.mli | 74 ++++ src/phl/rules/transforms/ecTrRCond.ml | 28 ++ src/phl/rules/transforms/ecTrRCond.mli | 26 ++ src/phl/rules/transforms/ecTrRMatch.ml | 30 ++ src/phl/rules/transforms/ecTrRMatch.mli | 27 ++ tests/rcond.ec | 329 ++++++++++++++++++ 29 files changed, 1726 insertions(+), 346 deletions(-) create mode 100644 src/phl/rules/bdhoare/ecBdHoareRCond.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareRCond.mli create mode 100644 src/phl/rules/bdhoare/ecBdHoareRMatch.ml create mode 100644 src/phl/rules/bdhoare/ecBdHoareRMatch.mli create mode 100644 src/phl/rules/ecPlRCond.ml create mode 100644 src/phl/rules/ecPlRCond.mli create mode 100644 src/phl/rules/ehoare/ecEHoareRCond.ml create mode 100644 src/phl/rules/ehoare/ecEHoareRCond.mli create mode 100644 src/phl/rules/ehoare/ecEHoareRMatch.ml create mode 100644 src/phl/rules/ehoare/ecEHoareRMatch.mli create mode 100644 src/phl/rules/equiv/ecEquivRCond.ml create mode 100644 src/phl/rules/equiv/ecEquivRCond.mli create mode 100644 src/phl/rules/equiv/ecEquivRMatch.ml create mode 100644 src/phl/rules/equiv/ecEquivRMatch.mli create mode 100644 src/phl/rules/hoare/ecHoareRCond.ml create mode 100644 src/phl/rules/hoare/ecHoareRCond.mli create mode 100644 src/phl/rules/hoare/ecHoareRMatch.ml create mode 100644 src/phl/rules/hoare/ecHoareRMatch.mli create mode 100644 src/phl/rules/transforms/ecTrRCond.ml create mode 100644 src/phl/rules/transforms/ecTrRCond.mli create mode 100644 src/phl/rules/transforms/ecTrRMatch.ml create mode 100644 src/phl/rules/transforms/ecTrRMatch.mli create mode 100644 tests/rcond.ec diff --git a/src/ecTyping.ml b/src/ecTyping.ml index 313fff050..ca3d015ba 100644 --- a/src/ecTyping.ml +++ b/src/ecTyping.ml @@ -2323,7 +2323,7 @@ and transmod_body ~attop (env : EcEnv.env) x params (me:pmodule_expr) = | None -> tyerror cp_loc env (InvalidModUpdate MUE_InvalidTargetCond) | Some (p, b) -> begin - (* TODO: Factorize. This is mostly just a copy/paste from EcPhlRCond.gen_rcond_full. *) + (* TODO: Factorize. This is mostly just a copy/paste from EcPlRCond.rmatch_select. *) let cvars = List.map (fun (x, xty) -> { ov_name = Some (EcIdent.name x); ov_type = xty; }) p in let me, cvars = EcMemory.bindall_fresh cvars !memenv in diff --git a/src/phl/README.md b/src/phl/README.md index acecbff3d..d200fc609 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, and later rcond, inline, swap, …) go through **one** trusted +(rndsem, rcond, and later inline, swap, …) go through **one** trusted transformation rule per logic, `t__transform` (`EcTransform`; equiv: one side at a time), parameterized by an entry of a catalogue: @@ -105,9 +105,11 @@ equiv: one side at a time), parameterized by an entry of a catalogue: ("-transform") re-runs it on the goal's program and compares the subgoals up to conversion (programs up to alpha-equivalence). -Current catalogue: `rndsem` (`EcTrRndSem`). Further entries come with the -tactics that use them. The framed form of `match C k` changes the -precondition: it stays a separate trusted rule. See `REFACTORING.md` §7f. +Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`) and +`rmatch` (`EcTrRMatch`). Further entries come with the tactics that use +them. The framed form of `match C k` changes the precondition: it stays a +separate trusted rule of each logic, `t__rmatch_framed` +(`EcRMatch`). See `REFACTORING.md` §7f. ## Directory layout @@ -123,7 +125,7 @@ src/phl/ Ec: one module per (logic, rule) transforms/ EcTr: catalogue entries of the program transformations ecPl*.ml computations shared by the rules of every logic: EcPlFrame, - EcPlSp, EcPlWp, EcPlRndSem, EcPlTransform + EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics diff --git a/src/phl/REFACTORING.md b/src/phl/REFACTORING.md index 0cd00567c..ae18315ce 100644 --- a/src/phl/REFACTORING.md +++ b/src/phl/REFACTORING.md @@ -151,8 +151,9 @@ src/phl/ ecPl*.ml logic-agnostic computations shared by the rules of every logic: EcPlFrame (framing conditions), EcPlSp (strongest postcondition), EcPlWp (weakest precondition), EcPlRndSem - (semantic sampling), EcPlTransform (the transformation - catalogue and its obligations) + (semantic sampling), EcPlRCond (deciding a conditional or + a match), EcPlTransform (the transformation catalogue and + its obligations) ecPlRecheck.ml checker scaffolding ecPhl.ml legacy: thin dispatchers and adapters, not-yet-migrated tactics @@ -351,7 +352,7 @@ parameterized by an entry of a **catalogue** of transformations: - equiv (transformation of side `i`): `forall &j, hoare [hd : P ==> cond]`, the relation read on side `i` with the other memory quantified. - These are the premises the `rcond` rules build today. + These are the premises `rcondt` / `rcondf` have always stated. - **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 @@ -363,18 +364,33 @@ parameterized by an entry of a **catalogue** of transformations: arguments, check what they always checked (to keep their error messages), and apply the transformation rule. -Current catalogue: `rndsem` (`EcTrRndSem`, semantic sampling of a -straight-line suffix, computed by `EcPlRndSem`; no obligation), used by the -`rndsem` tactic in hoare, bdhoare and equiv (no ehoare `rndsem`, so the -ehoare rule is not used yet). Further entries come with the tactics that use -them: rcond, rmatch, if/match-push, then swap, inline, kill/alias/cfold/set -and proc rewrite. +Current catalogue: +- `rndsem` (`EcTrRndSem`, semantic sampling of a straight-line suffix, + computed by `EcPlRndSem`; no obligation), used by the `rndsem` tactic in + hoare, bdhoare and equiv; +- `rcond` (`EcTrRCond`, deciding the `if` / `while` at a position; obligation + `OPrefixPost (hd, b)` or `OPrefixPost (hd, !b)`), used by `rcondt` / + `rcondf` in every logic; +- `rmatch` (`EcTrRMatch`, deciding the `match` at a position, the arguments + of the constructor being assigned to fresh program variables; obligation + `OPrefixPost (hd, exists xs, e = C xs)`), used by `match C k` in every + logic (its unframed form, see below). + +The decisions of a conditional or a match are computed by `EcPlRCond`. +Further entries come with the tactics that use them: if/match-push, then +swap, inline, kill/alias/cfold/set and proc rewrite. Exception: the framed form of `match C k` (used when the variables of the -discriminant `e` are neither read nor written by the prefix) adds `e = C ys` -to the precondition instead of assigning `ys` in the program. It changes the precondition, so it is not a program -transformation in this sense and stays a separate trusted rule (to be -rediscussed). +discriminant `e` are neither read nor written by the prefix, and the +judgement ignores the initial memories in which the prefix does not +terminate: hoare, ehoare, phoare `<=`, or an empty prefix) adds `e = C ys` +to the precondition instead of assigning `ys` in the program. It changes +the precondition, so it is not a program transformation in this sense and +stays a separate trusted rule of each logic, `t__rmatch_framed` +(`EcRMatch`, checker "-rmatch-framed"), stated on the whole +statement (to be rediscussed). The `match C k` tactic of each logic is +derived: it applies that rule when the framing condition holds, the +`rmatch` transformation otherwise. ## 8. Per-tactic migration recipe diff --git a/src/phl/ecPhlRCond.ml b/src/phl/ecPhlRCond.ml index b4e840abb..e86885b1a 100644 --- a/src/phl/ecPhlRCond.ml +++ b/src/phl/ecPhlRCond.ml @@ -1,350 +1,77 @@ (* -------------------------------------------------------------------- *) -open EcUtils -open EcSymbols open EcAst -open EcTypes -open EcDecl -open EcModules -open EcFol -open EcParsetree -open EcSubst open EcCoreGoal -open EcLowPhlGoal (* -------------------------------------------------------------------- *) -module Low = struct - (* ------------------------------------------------------------------ *) - let gen_rcond (pf, env) b m at_pos s = - let head, i, tail = s_split_i env at_pos s in - let e, s = - match i.i_node with - | Sif(e,s1,s2) -> e, if b then s1.s_node else s2.s_node - | Swhile(e,s1) -> e, if b then s1.s_node@[i] else [] - | _ -> - tc_error_lazy pf (fun fmt -> - Format.fprintf fmt - "the targetted instruction is not a conditionnal") - in - let f_e = ss_inv_of_expr m e in - let f_e = if b then f_e else map_ss_inv1 f_not f_e in - - (stmt head, e, f_e, stmt (head @ s @ tail)) - - (* ------------------------------------------------------------------ *) - let t_hoare_rcond_r b at_pos tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_hoareS tc in - let m = EcMemory.memory hs.hs_m in - let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.hs_s in - let e = update_hs_ss e (hs_po hs) in - let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd e in - let concl2 = f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs) in - FApi.xmutate1 tc `RCond [concl1; concl2] +(* The [rcond] and [match C k] tactics are derived, one module per logic in + [rules//] (EcHoareRCond, EcHoareRMatch, ...): they apply the + [rcond] / [rmatch] program transformations ([EcTrRCond], [EcTrRMatch]) + through the transformation rule of the logic, or the framed [rmatch] + rule of the logic. This module only keeps the legacy positional entry + points (adapters onto those tactics, so external callers and this + module's interface are unchanged) and the logic-agnostic dispatchers. *) - (* ------------------------------------------------------------------ *) - let t_ehoare_rcond_r b at_pos tc = - let env = FApi.tc1_env tc in - let hs = tc1_as_ehoareS tc in - let m = EcMemory.memory hs.ehs_m in - let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos hs.ehs_s in - let pre pr = - match destr_app pr with - | o, pre :: _ when f_equal o fop_interp_ehoare_form -> pre - | _ -> tc_error !!tc "the pre should have the form \"_ `|` _\"" in - let pre = map_ss_inv1 pre (ehs_pr hs) in - let e = POE.lift e in - - let concl1 = f_hoareS (snd hs.ehs_m) pre hd e in - let concl2 = f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs) in - FApi.xmutate1 tc `RCond [concl1; concl2] - - (* ------------------------------------------------------------------ *) - let t_bdhoare_rcond_r b at_pos tc = - let env = FApi.tc1_env tc in - let bhs = tc1_as_bdhoareS tc in - let m = EcMemory.memory bhs.bhs_m in - let hd,_,e,s = gen_rcond (!!tc, env) b m at_pos bhs.bhs_s in - let e = POE.lift e in +(* -------------------------------------------------------------------- *) +module Low = struct + let t_hoare_rcond b at_pos = + EcHoareRCond.(t_hoare_rcond { hrcr_at = at_pos; hrcr_branch = b }) - let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd e in - let concl2 = f_bdHoareS (snd bhs.bhs_m) (bhs_pr bhs) s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - FApi.xmutate1 tc `RCond [concl1; concl2] + let t_ehoare_rcond b at_pos = + EcEHoareRCond.(t_ehoare_rcond { ehrcr_at = at_pos; ehrcr_branch = b }) - (* ------------------------------------------------------------------ *) - let t_equiv_rcond_r side b at_pos tc = - let env = FApi.tc1_env tc in - let es = tc1_as_equivS tc in - let m,mo,s = - match side with - | `Left -> es.es_ml,es.es_mr, es.es_sl - | `Right -> es.es_mr,es.es_ml, es.es_sr in - let ts_inv_lower_side2 = sideif side ts_inv_lower_left2 ts_inv_lower_right2 in - let ss_inv_generalize_other = sideif side ss_inv_generalize_right ss_inv_generalize_left in - let hd,_,e,s = gen_rcond (!!tc, env) b (fst m) at_pos s in - let e = ss_inv_generalize_other e (fst mo) in - let concl1 = - EcSubst.f_forall_mems_ss_inv (EcIdent.create "&m", snd mo) - (ts_inv_lower_side2 (fun pr po -> - let mhs = EcIdent.create "&hr" in - let pr = ss_inv_rebind pr mhs in - let po = ss_inv_rebind po mhs in - let po = POE.lift po in - f_hoareS (snd m) pr hd po) (es_pr es) e) in - let sl,sr = match side with `Left -> s, es.es_sr | `Right -> es.es_sl, s in - let concl2 = f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) sl sr (es_po es) in - FApi.xmutate1 tc `RCond [concl1; concl2] + let t_bdhoare_rcond b at_pos = + EcBdHoareRCond.(t_bdhoare_rcond { brcr_at = at_pos; brcr_branch = b }) - (* ------------------------------------------------------------------ *) - let t_hoare_rcond = FApi.t_low2 "hoare-rcond" t_hoare_rcond_r - let t_ehoare_rcond = FApi.t_low2 "ehoare-rcond" t_ehoare_rcond_r - let t_bdhoare_rcond = FApi.t_low2 "bdhoare-rcond" t_bdhoare_rcond_r - let t_equiv_rcond = FApi.t_low3 "equiv-rcond" t_equiv_rcond_r + let t_equiv_rcond side b at_pos = + EcEquivRCond.(t_equiv_rcond + { ercr_side = side; ercr_at = at_pos; ercr_branch = b }) end (* -------------------------------------------------------------------- *) +(* Dispatch on the goal kind only. Without a side, a goal that is neither a + [bdHoareS] nor a [hoareS] goes to the ehoare tactic, which reports it. *) let t_rcond side b at_pos tc = - let concl = FApi.tc1_goal tc in - - match side with - | None when is_bdHoareS concl -> - Low.t_bdhoare_rcond b at_pos tc - | None when is_hoareS concl -> - Low.t_hoare_rcond b at_pos tc - | None -> - Low.t_ehoare_rcond b at_pos tc - | Some side -> - Low.t_equiv_rcond side b at_pos tc + match side, (FApi.tc1_goal tc).f_node with + | None, FbdHoareS _ -> Low.t_bdhoare_rcond b at_pos tc + | None, FhoareS _ -> Low.t_hoare_rcond b at_pos tc + | None, _ -> Low.t_ehoare_rcond b at_pos tc + | Some side, _ -> Low.t_equiv_rcond side b at_pos tc let process_rcond side b at_pos tc = - let at_pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, at_pos) in - t_rcond side b at_pos tc + match side, (FApi.tc1_goal tc).f_node with + | None, FbdHoareS _ -> EcBdHoareRCond.process_bdhoare_rcond b at_pos tc + | None, FhoareS _ -> EcHoareRCond.process_hoare_rcond b at_pos tc + | None, _ -> EcEHoareRCond.process_ehoare_rcond b at_pos tc + | Some side, _ -> EcEquivRCond.process_equiv_rcond side b at_pos tc (* -------------------------------------------------------------------- *) module LowMatch = struct - (* ------------------------------------------------------------------ *) - let gen_rcond (pf, env) c m at_pos s = - let head, i, tail = s_split_i env at_pos s in - let e, infos, (cvars, subs) = - match i.i_node with - | Smatch (e, bs) -> begin - let typ, tydc, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in - let tyd = oget (EcDecl.tydecl_as_datatype tydc) in - let ctor = - let test (_i : int) = sym_equal c -| fst in - List.Exceptionless.findi test tyd.tydt_ctors in - - match ctor with - | None -> - tc_error_lazy pf (fun fmt -> - Format.fprintf fmt - "cannot find the constructor %s" c) - - | Some (i, (cname, _cty)) -> - let b = oget (List.nth_opt bs i) in - let cname = EcPath.pqoname (EcPath.prefix typ) cname in - let tyinst = List.combine tydc.tyd_params tyinst in - (e, ((typ, tyd, tyinst), cname), b) - end - - | _ -> - tc_error_lazy pf (fun fmt -> - Format.fprintf fmt - "the targetted instruction is not a match") - in - - let f = ss_inv_of_expr m e in - - ((stmt head, subs, tail), (e, f), infos, cvars) - - (* [can_frame]: whether the judgement may use the framed form when the - prefix [hd] is not empty. The framed form adds [e = C ys] to the - precondition, which is only valid in the initial memories where [hd] - terminates: harmless for hoare, ehoare and phoare-[<=] judgements - (diverging runs carry no obligation, or contribute 0 to an upper - bound), unsound for phoare-[=]/[>=] and equiv ones. With an empty - prefix it is always sound. *) - let gen_rcond_full ~(can_frame : bool) (pf, env) c me0 at_pos s = - let m = EcMemory.memory me0 in - let (hd, s, tl), (e, f), ((typ, _tyd, tyinst), cname), cvars = - gen_rcond (pf,env) c m at_pos s in - - let po1 = - let names = List.map ( - fun (x, xty) -> - let x = - if EcIdent.name x = "_" - then EcIdent.create (symbol_of_ty xty) - else EcIdent.fresh x - in (x, xty)) cvars in - let vars = List.map (curry f_local) names in - let cty = toarrow (List.snd names) f.inv.f_ty in - let po = f_op cname (List.snd tyinst) cty in - let po = f_app po vars f.inv.f_ty in - map_ss_inv1 (f_exists (List.map (snd_map gtty) names)) (map_ss_inv2 f_eq f {m;inv=po}) in - - let me, pvs = - let cvars = - List.map - (fun (x, xty) -> { ov_name = Some (EcIdent.name x); ov_type = xty; }) - cvars in - EcMemory.bindall_fresh cvars me0 in - - let subst, pvs = - let s = Fsubst.f_subst_id in - let s, pvs = - List.fold_left_map (fun s ((x, xty), name) -> - let pv = pv_loc (oget name.ov_name) in - let s = bind_elocal s x (e_var pv xty) in - (s, (pv, xty))) - s (List.combine cvars pvs) in - (s, pvs) in - - let frame = - (can_frame || List.is_empty hd.s_node) - && EcPV.PV.indep env - (EcPV.e_read env e) - (EcPV.PV.union (EcPV.s_read env hd) (EcPV.s_write env hd)) in - - let epr, asgn = - if frame then begin - let vars = List.map (fun (pv, ty) -> f_pvar pv ty (fst me)) pvs in - let epr = f_op cname (List.snd tyinst) f.inv.f_ty in - let epr = map_ss_inv ~m:f.m (fun vars -> f_app epr vars f.inv.f_ty) vars in - Some (map_ss_inv2 f_eq f epr), [] - end else begin - let asgn = - EcModules.lv_of_list pvs |> omap (fun lv -> - (* FIXME: factorize out *) - let rty = ttuple (List.snd cvars) in - let proj = EcInductive.datatype_proj_path typ (EcPath.basename cname) in - let proj = e_op proj (List.snd tyinst) (tfun e.e_ty (toption rty)) in - let proj = e_app proj [e] (toption rty) in - let proj = e_oget proj rty in - i_asgn (lv, proj)) in - None, otolist asgn - end in - - (epr, hd, po1), (me, stmt (hd.s_node @ asgn @ (s_subst subst s).s_node @ tl)) - - (* ------------------------------------------------------------------ *) - let t_hoare_rcond_match_r c at_pos tc = - let hs = tc1_as_hoareS tc in - let (epr, hd, po1), (me, full) = - gen_rcond_full ~can_frame:true (!!tc, FApi.tc1_env tc) c hs.hs_m at_pos hs.hs_s in - - let pr = ofold (map_ss_inv2 f_and) (hs_pr hs) epr in - let po1 = update_hs_ss po1 (hs_po hs) in - - let concl1 = f_hoareS (snd hs.hs_m) (hs_pr hs) hd po1 in - let concl2 = f_hoareS (snd me) pr full (hs_po hs) in + let t_hoare_rcond_match c at_pos = + EcHoareRMatch.(t_hoare_rmatch { hrmr_at = at_pos; hrmr_ctor = c }) - FApi.xmutate1 tc `RCondMatch [concl1; concl2] + let t_bdhoare_rcond_match c at_pos = + EcBdHoareRMatch.(t_bdhoare_rmatch { brmr_at = at_pos; brmr_ctor = c }) - (* ------------------------------------------------------------------ *) - let t_ehoare_rcond_match_r c at_pos tc = - let hs = tc1_as_ehoareS tc in - let (epr, hd, po1), (me, full) = - gen_rcond_full ~can_frame:true (!!tc, FApi.tc1_env tc) c hs.ehs_m at_pos hs.ehs_s in - - (* The precondition has the form [P `|` f], with [P] boolean: as for - [rcond], the prefix obligation is a hoare judgement on [P], and the - framed condition is added to [P]. *) - let p, f = - match destr_app (ehs_pr hs).inv with - | o, [p; f] when f_equal o fop_interp_ehoare_form -> p, f - | _ -> tc_error !!tc "the pre should have the form \"_ `|` _\"" in - let p = { m = (ehs_pr hs).m; inv = p; } in - let pr = - map_ss_inv1 (fun p -> f_interp_ehoare_form p f) - (ofold (map_ss_inv2 f_and) p epr) in - - let concl1 = f_hoareS (snd hs.ehs_m) p hd (POE.lift po1) in - let concl2 = f_eHoareS (snd me) pr full (ehs_po hs) in - - FApi.xmutate1 tc `RCondMatch [concl1; concl2] - - (* ------------------------------------------------------------------ *) - let t_bdhoare_rcond_match_r c at_pos tc = - let bhs = tc1_as_bdhoareS tc in - let (epr, hd, po1), (me, full) = - gen_rcond_full ~can_frame:(bhs.bhs_cmp = FHle) - (!!tc, FApi.tc1_env tc) c bhs.bhs_m at_pos bhs.bhs_s in - - let pr = ofold (map_ss_inv2 f_and) (bhs_pr bhs) epr in - let po1 = POE.lift po1 in - - let concl1 = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) hd po1 in - let concl2 = f_bdHoareS (snd me) pr full (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in - - FApi.xmutate1 tc `RCondMatch [concl1; concl2] - - (* ------------------------------------------------------------------ *) - let t_equiv_rcond_match_r side c at_pos tc = - let es = tc1_as_equivS tc in - let ml, mr = fst es.es_ml, fst es.es_mr in - - let m, mo, s = - match side with - | `Left -> es.es_ml, es.es_mr, es.es_sl - | `Right -> es.es_mr, es.es_ml, es.es_sr in - - let (epr, hd, po1), (me, full) = - gen_rcond_full ~can_frame:false (!!tc, FApi.tc1_env tc) c m at_pos s in - - let ss_inv_generalize_other inv = sideif side - (ss_inv_generalize_right inv mr) (ss_inv_generalize_left inv ml) in - - let epr = omap (fun epr -> - ss_inv_generalize_other (ss_inv_rebind epr (fst m))) epr in - - let ts_inv_lower_side1 = - sideif side ts_inv_lower_left1 ts_inv_lower_right1 in - - let po1 = POE.lift po1 in - let concl1 = - f_forall_mems_ss_inv mo - (ts_inv_lower_side1 (fun pr -> f_hoareS (snd m) pr hd po1) (es_pr es)) in - - let (ml, mr), (sl, sr) = - match side with - | `Left -> - ((fst es.es_ml, snd me), es.es_mr), - (full, es.es_sr) - - | `Right -> - (es.es_ml, (fst es.es_mr, snd me)), - (es.es_sl, full) in - - let concl2 = - f_equivS (snd ml) (snd mr) (ofold (map_ts_inv2 f_and) (es_pr es) epr) sl sr (es_po es) in - FApi.xmutate1 tc `RCond [concl1; concl2] - - (* ------------------------------------------------------------------ *) - let t_hoare_rcond_match = - FApi.t_low2 "hoare-rcond-match" t_hoare_rcond_match_r - - let t_ehoare_rcond_match = - FApi.t_low2 "hoare-rcond-match" t_ehoare_rcond_match_r - - let t_bdhoare_rcond_match = - FApi.t_low2 "hoare-rcond-match" t_bdhoare_rcond_match_r - - let t_equiv_rcond_match = - FApi.t_low3 "hoare-rcond-match" t_equiv_rcond_match_r + let t_equiv_rcond_match side c at_pos = + EcEquivRMatch.(t_equiv_rmatch + { ermr_side = side; ermr_at = at_pos; ermr_ctor = c }) end (* -------------------------------------------------------------------- *) +(* Dispatch on the goal kind only. Without a side, a goal that is neither a + [bdHoareS] nor an [eHoareS] goes to the hoare tactic, which reports it. *) let t_rcond_match side c at_pos tc = - let concl = FApi.tc1_goal tc in + match side, (FApi.tc1_goal tc).f_node with + | None, FbdHoareS _ -> LowMatch.t_bdhoare_rcond_match c at_pos tc + | None, FeHoareS _ -> + EcEHoareRMatch.(t_ehoare_rmatch { ehrmr_at = at_pos; ehrmr_ctor = c }) tc + | None, _ -> LowMatch.t_hoare_rcond_match c at_pos tc + | Some side, _ -> LowMatch.t_equiv_rcond_match side c at_pos tc - match side with - | None when is_bdHoareS concl -> LowMatch.t_bdhoare_rcond_match c at_pos tc - | None when is_eHoareS concl -> LowMatch.t_ehoare_rcond_match c at_pos tc - | None -> LowMatch.t_hoare_rcond_match c at_pos tc - | Some side -> LowMatch.t_equiv_rcond_match side c at_pos tc - -(* -------------------------------------------------------------------- *) let process_rcond_match side c at_pos tc = - let at_pos = EcLowPhlGoal.tc1_process_codepos1 tc (side, at_pos) in - t_rcond_match side c at_pos tc + match side, (FApi.tc1_goal tc).f_node with + | None, FbdHoareS _ -> EcBdHoareRMatch.process_bdhoare_rmatch c at_pos tc + | None, FeHoareS _ -> EcEHoareRMatch.process_ehoare_rmatch c at_pos tc + | None, _ -> EcHoareRMatch.process_hoare_rmatch c at_pos tc + | Some side, _ -> EcEquivRMatch.process_equiv_rmatch side c at_pos tc diff --git a/src/phl/rules/bdhoare/ecBdHoareRCond.ml b/src/phl/rules/bdhoare/ecBdHoareRCond.ml new file mode 100644 index 000000000..f33f27107 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRCond.ml @@ -0,0 +1,28 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [rcond] tactic as supplied by the caller: high + level, the position is still symbolic and must be resolved. *) +type bdhoare_rcond_rule = { + brcr_at : EcMatching.Position.codepos1; (* position of the conditional *) + brcr_branch : bool; (* branch taken *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position (failing as before the + migration when it is invalid or not a conditional) and apply the + [rcond] transformation through the bdhoare transformation rule. *) +let t_bdhoare_rcond (r : bdhoare_rcond_rule) (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let at = EcPlRCond.resolve_rcond !!tc (FApi.tc1_env tc) r.brcr_at bhs.bhs_s in + let tr = EcTrRCond.TrRCond { trrc_at = at; trrc_branch = r.brcr_branch } in + EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. Type the position in + its memory, then apply the tactic. *) +let process_bdhoare_rcond (b : bool) (at : EcParsetree.pcodepos1) (tc : tcenv1) = + let at = tc1_process_codepos1 tc (None, at) in + t_bdhoare_rcond { brcr_at = at; brcr_branch = b } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareRCond.mli b/src/phl/rules/bdhoare/ecBdHoareRCond.mli new file mode 100644 index 000000000..d00fe14e3 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRCond.mli @@ -0,0 +1,35 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Derived tactics *) + +type bdhoare_rcond_rule = { + brcr_at : codepos1; (* position k of the conditional *) + brcr_branch : bool; (* branch b taken *) +} + +(* [t_bdhoare_rcond { brcr_at = k; brcr_branch = b }] — decides the + conditional [i = c[k]] of [phoare [c : P ==> Q] ~ d], with + [c = hd; i; tl]. Resolves [k] to an index (failing with "invalid split + index" when it is invalid, then with "the targetted instruction is not a + conditionnal" when [i] is neither an [if] nor a [while]), then applies + + [EcBdHoareTransform.t_bdhoare_transform] with + [EcTrRCond.TrRCond { trrc_at = k (resolved); trrc_branch = b }] + + Visible goals, in this order (those of the rule): + hoare [hd : P ==> e] (b = true; [!e] when b = false) + phoare [c' : P ==> Q] ~ d + with [c'] the decided statement (see [EcTrRCond]). Emits no node of its + own. *) +val t_bdhoare_rcond : bdhoare_rcond_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rcondt k] / [rcondf k] on a [bdHoareS] goal: types the position [k] in + the goal's memory and applies [t_bdhoare_rcond]. *) +val process_bdhoare_rcond : bool -> pcodepos1 -> backward diff --git a/src/phl/rules/bdhoare/ecBdHoareRMatch.ml b/src/phl/rules/bdhoare/ecBdHoareRMatch.ml new file mode 100644 index 000000000..8f88577e8 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRMatch.ml @@ -0,0 +1,92 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the framed bdhoare [rmatch] rule, resolved: the position + of the match and its constructor are integer indices. Nothing to + resolve: the same record is the rule argument and the node payload. *) +type bdhoare_rmatch_framed = { + brmf_at : EcMatching.Position.nm_codepos1; (* position of the match *) + brmf_ctor : int; (* index of the constructor *) +} + +type EcCoreGoal.rule += RBdHoareRMatchFramed of bdhoare_rmatch_framed + +(* -------------------------------------------------------------------- *) +(* The framed form ignores the initial memories in which the prefix does + not terminate: sound for an upper bound only, unless the prefix is + empty. *) +let can_frame (bhs : bdHoareS) = bhs.bhs_cmp = FHle + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + instruction is a [match] with that constructor, the framing condition) + are re-checked here, from the goal: the checker re-validates them. *) +let bdhoare_rmatch_framed_subgoals + (hyps : LDecl.hyps) (bhs : bdHoareS) (n : bdhoare_rmatch_framed) += + let env = LDecl.toenv hyps in + let r = EcPlRCond.rmatch_select env bhs.bhs_m n.brmf_at n.brmf_ctor bhs.bhs_s in + if not (EcPlRCond.rmatch_can_frame env ~can_frame:(can_frame bhs) n.brmf_at bhs.bhs_s) then + raise (InvalidTransform "the framed form of match does not apply"); + let a = f_hoareS (snd bhs.bhs_m) (bhs_pr bhs) r.rm_hd (POE.lift r.rm_post) in + let b = f_bdHoareS (snd r.rm_me) (map_ss_inv2 f_and r.rm_eq (bhs_pr bhs)) + r.rm_framed (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). A side condition that does not hold is reported as a tactic + error. *) +let t_bdhoare_rmatch_framed (n : bdhoare_rmatch_framed) (tc : tcenv1) = + let bhs = tc1_as_bdhoareS tc in + let sg = + try bdhoare_rmatch_framed_subgoals (FApi.tc1_hyps tc) bhs n + with InvalidTransform msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RBdHoareRMatchFramed n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RBdHoareRMatchFramed n -> + Some (EcPlRecheck.checker_of "bdhoare-rmatch-framed" pf_as_bdhoareS + (fun hyps bhs -> bdhoare_rmatch_framed_subgoals hyps bhs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Parameters of the bdhoare [rmatch] tactic as supplied by the caller: + high level, the position and the constructor are still symbolic. *) +type bdhoare_rmatch_rule = { + brmr_at : EcMatching.Position.codepos1; (* position of the match *) + brmr_ctor : EcSymbols.symbol; (* constructor of the branch *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position and the constructor + (failing as before the migration), then apply the framed rule when the + framing condition holds, the [rmatch] transformation through the + bdhoare transformation rule otherwise. *) +let t_bdhoare_rmatch (r : bdhoare_rmatch_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let bhs = tc1_as_bdhoareS tc in + let at, j = EcPlRCond.resolve_rmatch !!tc env r.brmr_at r.brmr_ctor bhs.bhs_s in + if EcPlRCond.rmatch_can_frame env ~can_frame:(can_frame bhs) at bhs.bhs_s then + t_bdhoare_rmatch_framed { brmf_at = at; brmf_ctor = j } tc + else + let tr = EcTrRMatch.TrRMatch { trrm_at = at; trrm_ctor = j } in + EcBdHoareTransform.t_bdhoare_transform { btr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [bdHoareS]. Type the position in + its memory, then apply the tactic. *) +let process_bdhoare_rmatch + (c : EcSymbols.symbol) (at : EcParsetree.pcodepos1) (tc : tcenv1) += + let at = tc1_process_codepos1 tc (None, at) in + t_bdhoare_rmatch { brmr_at = at; brmr_ctor = c } tc diff --git a/src/phl/rules/bdhoare/ecBdHoareRMatch.mli b/src/phl/rules/bdhoare/ecBdHoareRMatch.mli new file mode 100644 index 000000000..da5b980b9 --- /dev/null +++ b/src/phl/rules/bdhoare/ecBdHoareRMatch.mli @@ -0,0 +1,77 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type bdhoare_rmatch_framed = { + brmf_at : nm_codepos1; (* position k of the match (resolved) *) + brmf_ctor : int; (* index j of the constructor C *) +} + +(* [t_bdhoare_rmatch_framed { brmf_at = k; brmf_ctor = j }] — framed form + of [match C k]. With [c = hd; i; tl], [hd = c[0..k)] and + [i = c[k] = match e with ... | C xs => b | ...], [C] its [j]-th + constructor, and [~] the goal's comparison: + + hoare [hd : P ==> exists xs, e = C xs] + phoare [hd; b[ys/xs]; tl : e = C ys /\ P ==> Q] ~ d + ----------------------------------------------------- e indep. of hd, + phoare [c : P ==> Q] ~ d ~ is <= or hd = [] + + where [ys] are fresh program variables, added to the memory of the + second premise. Side conditions: [i] is a [match] with a [j]-th + constructor; the variables read by [e] are neither read nor written by + [hd]; [~] is [<=] or [hd] is empty. + + This is not a program transformation: [e = C ys] goes to the + precondition, so the rule is stated on the whole statement (implicit + seq around the match). It is retained as a separate rule pending a + later discussion (the unframed form of [match C k] is the program + transformation [EcTrRMatch]). It is sound because [e] has the same + value before and after [hd], and because, in an initial memory in which + [hd] does not terminate, the probability of [Q] is 0, below any upper + bound: in the other ones, the first premise yields [ys] with + [e = C ys] initially. For [=] and [>=], such a memory is not covered by + the second premise, hence the restriction to an empty prefix. + + Node: [RBdHoareRMatchFramed { brmf_at = k; brmf_ctor = j }]. + Checker: "bdhoare-rmatch-framed" (it re-checks the side conditions). *) +val t_bdhoare_rmatch_framed : bdhoare_rmatch_framed -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +type bdhoare_rmatch_rule = { + brmr_at : codepos1; (* position k of the match *) + brmr_ctor : symbol; (* constructor C of the branch taken *) +} + +(* [t_bdhoare_rmatch { brmr_at = k; brmr_ctor = C }] — decides the match + [i = c[k]] of [phoare [c : P ==> Q] ~ d] in favour of its [C] branch. + Resolves [k] to an index and [C] to its index [j] (failing with "invalid + split index", "the targetted instruction is not a match", "cannot find + the constructor C", in this order), then applies: + - when the variables read by [e] are neither read nor written by the + prefix [hd], and [~] is [<=] or [hd] is empty (framed form): + [t_bdhoare_rmatch_framed { k; j }]; + - otherwise (unframed form): [EcBdHoareTransform.t_bdhoare_transform] + with [EcTrRMatch.TrRMatch { trrm_at = k; trrm_ctor = j }]. + + Visible goals, in this order (those of the rule applied): + hoare [hd : P ==> exists xs, e = C xs] + phoare [hd; b[ys/xs]; tl : e = C ys /\ P ==> Q] ~ d (framed) + phoare [hd; ys <- oget (get_as_C e); b[ys/xs]; tl : P ==> Q] ~ d + (unframed) + Emits no node of its own. *) +val t_bdhoare_rmatch : bdhoare_rmatch_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match C k] on a [bdHoareS] goal: types the position [k] in the goal's + memory and applies [t_bdhoare_rmatch]. *) +val process_bdhoare_rmatch : symbol -> pcodepos1 -> backward diff --git a/src/phl/rules/ecPlRCond.ml b/src/phl/rules/ecPlRCond.ml new file mode 100644 index 000000000..e9141e92b --- /dev/null +++ b/src/phl/rules/ecPlRCond.ml @@ -0,0 +1,157 @@ +(* -------------------------------------------------------------------- *) +open EcUtils +open EcSymbols +open EcAst +open EcTypes +open EcModules +open EcFol + +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* The instruction at the resolved index [k] of [s], with the prefix (in + order) and the suffix. *) +let split_at (k : EcMatching.Position.nm_codepos1) (s : stmt) = + try EcMatching.Position.find_by_nmcpos1 ~rev:false k s + with EcMatching.Position.InvalidCPos -> + raise (InvalidTransform "invalid instruction index") + +(* -------------------------------------------------------------------- *) +let rcond_select (m : memory) k (b : bool) (s : stmt) = + let hd, i, tl = split_at k s in + let e, s = + match i.i_node with + | Sif (e, s1, s2) -> e, if b then s1.s_node else s2.s_node + | Swhile (e, s1) -> e, if b then s1.s_node @ [i] else [] + | _ -> raise (InvalidTransform "the targetted instruction is not a conditionnal") in + let g = ss_inv_of_expr m e in + let g = if b then g else map_ss_inv1 f_not g in + (stmt hd, g, stmt (hd @ s @ tl)) + +(* -------------------------------------------------------------------- *) +type rmatch = { + rm_hd : stmt; + rm_post : ss_inv; + rm_me : memenv; + rm_eq : ss_inv; + rm_framed : stmt; + rm_unframed : stmt; +} + +let rmatch_select (env : EcEnv.env) (me0 : memenv) k (j : int) (s : stmt) = + let m = EcMemory.memory me0 in + let hd, i, tl = split_at k s in + let e, bs = + match i.i_node with + | Smatch (e, bs) -> e, bs + | _ -> raise (InvalidTransform "the targetted instruction is not a match") in + let typ, tydc, tyinst = oget (EcEnv.Ty.get_top_decl e.e_ty env) in + let tyd = oget (EcDecl.tydecl_as_datatype tydc) in + let (cname, _), (cvars, b) = + try List.nth tyd.tydt_ctors j, List.nth bs j + with Invalid_argument _ | Failure _ -> + raise (InvalidTransform "invalid constructor index") in + let cname = EcPath.pqoname (EcPath.prefix typ) cname in + let tyinst = List.combine tydc.tyd_params tyinst in + let f = ss_inv_of_expr m e in + + (* exists xs, e = C xs *) + let post = + let names = List.map ( + fun (x, xty) -> + let x = + if EcIdent.name x = "_" + then EcIdent.create (symbol_of_ty xty) + else EcIdent.fresh x + in (x, xty)) cvars in + let vars = List.map (curry f_local) names in + let cty = toarrow (List.snd names) f.inv.f_ty in + let po = f_op cname (List.snd tyinst) cty in + let po = f_app po vars f.inv.f_ty in + map_ss_inv1 (f_exists (List.map (snd_map gtty) names)) (map_ss_inv2 f_eq f {m;inv=po}) in + + (* The arguments [xs] of [C] become fresh program variables [ys]. *) + let me, pvs = + let cvars = + List.map + (fun (x, xty) -> { ov_name = Some (EcIdent.name x); ov_type = xty; }) + cvars in + EcMemory.bindall_fresh cvars me0 in + + let subst, pvs = + List.fold_left_map (fun s ((x, xty), name) -> + let pv = pv_loc (oget name.ov_name) in + let s = bind_elocal s x (e_var pv xty) in + (s, (pv, xty))) + Fsubst.f_subst_id (List.combine cvars pvs) in + + let b = (s_subst subst b).s_node in + + (* Framed form: e = C ys *) + let eq = + let vars = List.map (fun (pv, ty) -> f_pvar pv ty (fst me)) pvs in + let epr = f_op cname (List.snd tyinst) f.inv.f_ty in + let epr = map_ss_inv ~m:f.m (fun vars -> f_app epr vars f.inv.f_ty) vars in + map_ss_inv2 f_eq f epr in + + (* Unframed form: ys <- oget (get_as_C e) *) + let asgn = + EcModules.lv_of_list pvs |> omap (fun lv -> + let rty = ttuple (List.snd cvars) in + let proj = EcInductive.datatype_proj_path typ (EcPath.basename cname) in + let proj = e_op proj (List.snd tyinst) (tfun e.e_ty (toption rty)) in + let proj = e_app proj [e] (toption rty) in + let proj = e_oget proj rty in + i_asgn (lv, proj)) in + + { rm_hd = stmt hd; + rm_post = post; + rm_me = me; + rm_eq = eq; + rm_framed = stmt (hd @ b @ tl); + rm_unframed = stmt (hd @ otolist asgn @ b @ tl); } + +(* -------------------------------------------------------------------- *) +let rmatch_can_frame (env : EcEnv.env) ~(can_frame : bool) k (s : stmt) = + match split_at k s with + | hd, { i_node = Smatch (e, _); _ }, _ -> + let hd = stmt hd in + (can_frame || List.is_empty hd.s_node) + && EcPV.PV.indep env + (EcPV.e_read env e) + (EcPV.PV.union (EcPV.s_read env hd) (EcPV.s_write env hd)) + | _ -> false + | exception InvalidTransform _ -> false + +(* -------------------------------------------------------------------- *) +let resolve_at (env : EcEnv.env) (at : EcMatching.Position.codepos1) (s : stmt) = + let module Pos = EcMatching.Position in + try + let k = Pos.normalize_cpos1 env at s in + let _, i, _ = Pos.find_by_nmcpos1 ~rev:false k s in + (k, i) + with Pos.InvalidCPos -> raise (EcLowPhlGoal.InvalidSplit (`Instr at)) + +let resolve_rcond pe env at s = + let k, i = resolve_at env at s in + match i.i_node with + | Sif _ | Swhile _ -> k + | _ -> + EcCoreGoal.tc_error_lazy pe (fun fmt -> + Format.fprintf fmt "the targetted instruction is not a conditionnal") + +let resolve_rmatch pe env at (c : symbol) s = + let k, i = resolve_at env at s in + match i.i_node with + | Smatch (e, _) -> begin + let _, tydc, _ = oget (EcEnv.Ty.get_top_decl e.e_ty env) in + let tyd = oget (EcDecl.tydecl_as_datatype tydc) in + match List.Exceptionless.findi (fun _ -> sym_equal c -| fst) tyd.tydt_ctors with + | Some (j, _) -> (k, j) + | None -> + EcCoreGoal.tc_error_lazy pe (fun fmt -> + Format.fprintf fmt "cannot find the constructor %s" c) + end + | _ -> + EcCoreGoal.tc_error_lazy pe (fun fmt -> + Format.fprintf fmt "the targetted instruction is not a match") diff --git a/src/phl/rules/ecPlRCond.mli b/src/phl/rules/ecPlRCond.mli new file mode 100644 index 000000000..5ddf07d2d --- /dev/null +++ b/src/phl/rules/ecPlRCond.mli @@ -0,0 +1,76 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcAst +open EcEnv +open EcMatching.Position + +(* -------------------------------------------------------------------- *) +(* Deciding a conditional ([if] / [while]) or a [match] at a given position + of a statement, shared by the [rcond] and [rmatch] transformations + ([EcTrRCond], [EcTrRMatch]), by the framed [rmatch] rules + ([EcRMatch]) and by the tactics using them. + + The statement is [c = hd; i; tl], where [i = c[k]] is the instruction at + the resolved index [k] and [hd = c[0..k)]. The computations are pure: + positions are resolved indices, so the statement is never searched; they + raise [EcPlTransform.InvalidTransform] when [i] is not of the expected + form. *) + +(* -------------------------------------------------------------------- *) +(* [rcond_select m k b c] decides the conditional [i] in favour of the + branch [b]. Returns [(hd, g, c')] where, in memory [m]: + + i b g c' + if e then s1 else s2 true e hd; s1; tl + if e then s1 else s2 false !e hd; s2; tl + while e do s1 true e hd; s1; while e do s1; tl + while e do s1 false !e hd; tl + + Fails with "the targetted instruction is not a conditionnal" if [i] is + neither an [if] nor a [while]. *) +val rcond_select : memory -> nm_codepos1 -> bool -> stmt -> stmt * ss_inv * stmt + +(* -------------------------------------------------------------------- *) +(* The decomposition of [c] at [i = match e with ... | C xs => b | ...], + decided in favour of its [j]-th constructor [C]: *) +type rmatch = { + rm_hd : stmt; (* hd *) + rm_post : ss_inv; (* exists xs, e = C xs (in the memory of [c]) *) + rm_me : memenv; (* the memory of [c], extended with fresh program + variables [ys] for [xs] *) + rm_eq : ss_inv; (* e = C ys (framed form) *) + rm_framed : stmt; (* hd; b[ys/xs]; tl (framed form) *) + rm_unframed : stmt; (* hd; ys <- oget (get_as_C e); b[ys/xs]; tl + (no assignment when [C] has no argument) *) +} + +(* [rmatch_select env me k j c]: the decomposition above, [me] being the + memory of [c]. Fails with "the targetted instruction is not a match" if + [i] is not a [match], or "invalid constructor index" if it has no + [j]-th branch. *) +val rmatch_select : env -> memenv -> nm_codepos1 -> int -> stmt -> rmatch + +(* [rmatch_can_frame env ~can_frame k c]: whether the framed form of + [rmatch] applies to the [match] [i] (false if [i] is not a [match]): + the variables read by [e] are neither read nor written by [hd] (so that + [e] has the same value before and after [hd]), and [can_frame] holds or + [hd] is empty. [can_frame] is given by the logic: the framed form is + only sound for judgements that ignore the initial memories in which + [hd] does not terminate (see [EcRMatch]). *) +val rmatch_can_frame : env -> can_frame:bool -> nm_codepos1 -> stmt -> bool + +(* -------------------------------------------------------------------- *) +(* Resolution, tactic side (never used by the rules or their checkers): + resolve the position [k] in [c] and check the instruction, with the + user-facing error messages, in this order: invalid position + ([EcLowPhlGoal.InvalidSplit]), then the instruction is not of the + expected form, then (rmatch) no constructor named [C]. *) + +(* [resolve_rcond pe env k c]: the index of the conditional at [k]. *) +val resolve_rcond : + EcCoreGoal.proofenv -> env -> codepos1 -> stmt -> nm_codepos1 + +(* [resolve_rmatch pe env k C c]: the index of the [match] at [k], and the + index of [C] among the constructors of its datatype. *) +val resolve_rmatch : + EcCoreGoal.proofenv -> env -> codepos1 -> symbol -> stmt -> nm_codepos1 * int diff --git a/src/phl/rules/ecPlTransform.mli b/src/phl/rules/ecPlTransform.mli index e83bf8cb8..6696a3160 100644 --- a/src/phl/rules/ecPlTransform.mli +++ b/src/phl/rules/ecPlTransform.mli @@ -29,7 +29,11 @@ open EcEnv logic's rule states them as premises of its own (see its [.mli]). Current catalogue: [EcTrRndSem] (semantic sampling of a straight-line - suffix). Entries live in [rules/transforms/], as [EcTr]. *) + suffix), [EcTrRCond] (deciding an [if] / [while]) and [EcTrRMatch] + (deciding a [match], its unframed form). 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]). *) (* -------------------------------------------------------------------- *) (* An entry of the catalogue, with its resolved parameters. *) diff --git a/src/phl/rules/ehoare/ecEHoareRCond.ml b/src/phl/rules/ehoare/ecEHoareRCond.ml new file mode 100644 index 000000000..e6acef8d0 --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRCond.ml @@ -0,0 +1,30 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [rcond] tactic as supplied by the caller: high + level, the position is still symbolic and must be resolved. *) +type ehoare_rcond_rule = { + ehrcr_at : EcMatching.Position.codepos1; (* position of the conditional *) + ehrcr_branch : bool; (* branch taken *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position (failing as before the + migration when it is invalid or not a conditional) and apply the + [rcond] transformation through the ehoare transformation rule (which + checks the form of the precondition). *) +let t_ehoare_rcond (r : ehoare_rcond_rule) (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let at = EcPlRCond.resolve_rcond !!tc (FApi.tc1_env tc) r.ehrcr_at hs.ehs_s in + let tr = EcTrRCond.TrRCond { trrc_at = at; trrc_branch = r.ehrcr_branch } in + EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS] (or is reported as not + being one when typing the position). Type the position in its memory, + then apply the tactic. *) +let process_ehoare_rcond (b : bool) (at : EcParsetree.pcodepos1) (tc : tcenv1) = + let at = tc1_process_codepos1 tc (None, at) in + t_ehoare_rcond { ehrcr_at = at; ehrcr_branch = b } tc diff --git a/src/phl/rules/ehoare/ecEHoareRCond.mli b/src/phl/rules/ehoare/ecEHoareRCond.mli new file mode 100644 index 000000000..48a3211ec --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRCond.mli @@ -0,0 +1,37 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Derived tactics *) + +type ehoare_rcond_rule = { + ehrcr_at : codepos1; (* position k of the conditional *) + ehrcr_branch : bool; (* branch b taken *) +} + +(* [t_ehoare_rcond { ehrcr_at = k; ehrcr_branch = b }] — decides the + conditional [i = c[k]] of [ehoare [c : P `|` f ==> Q]], with + [c = hd; i; tl]. Resolves [k] to an index (failing with "invalid split + index" when it is invalid, then with "the targetted instruction is not a + conditionnal" when [i] is neither an [if] nor a [while]), then applies + + [EcEHoareTransform.t_ehoare_transform] with + [EcTrRCond.TrRCond { trrc_at = k (resolved); trrc_branch = b }] + + (failing with "the pre should have the form \"_ `|` _\"" otherwise). + + Visible goals, in this order (those of the rule): + hoare [hd : P ==> e] (b = true; [!e] when b = false) + ehoare [c' : P `|` f ==> Q] + with [c'] the decided statement (see [EcTrRCond]). Emits no node of its + own. *) +val t_ehoare_rcond : ehoare_rcond_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rcondt k] / [rcondf k] on an [eHoareS] goal: types the position [k] in + the goal's memory and applies [t_ehoare_rcond]. *) +val process_ehoare_rcond : bool -> pcodepos1 -> backward diff --git a/src/phl/rules/ehoare/ecEHoareRMatch.ml b/src/phl/rules/ehoare/ecEHoareRMatch.ml new file mode 100644 index 000000000..5ba2245ad --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRMatch.ml @@ -0,0 +1,94 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the framed ehoare [rmatch] rule, resolved: the position of + the match and its constructor are integer indices. Nothing to resolve: + the same record is the rule argument and the node payload. *) +type ehoare_rmatch_framed = { + ehrmf_at : EcMatching.Position.nm_codepos1; (* position of the match *) + ehrmf_ctor : int; (* index of the constructor *) +} + +type EcCoreGoal.rule += REHoareRMatchFramed of ehoare_rmatch_framed + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + instruction is a [match] with that constructor, the framing condition, + the form [P `|` f] of the precondition) are re-checked here, from the + goal: the checker re-validates them. The prefix obligation is a hoare + judgement on [P], and [e = C ys] is added to [P]. *) +let ehoare_rmatch_framed_subgoals + (hyps : LDecl.hyps) (hs : eHoareS) (n : ehoare_rmatch_framed) += + let env = LDecl.toenv hyps in + let r = EcPlRCond.rmatch_select env hs.ehs_m n.ehrmf_at n.ehrmf_ctor hs.ehs_s in + if not (EcPlRCond.rmatch_can_frame env ~can_frame:true n.ehrmf_at hs.ehs_s) then + raise (InvalidTransform "the framed form of match does not apply"); + let p, f = + match destr_app (ehs_pr hs).inv with + | o, [p; f] when f_equal o fop_interp_ehoare_form -> p, f + | _ -> raise (InvalidTransform "the pre should have the form \"_ `|` _\"") in + let p = { m = (ehs_pr hs).m; inv = p; } in + let pr = map_ss_inv1 (fun p -> f_interp_ehoare_form p f) (map_ss_inv2 f_and r.rm_eq p) in + let a = f_hoareS (snd hs.ehs_m) p r.rm_hd (POE.lift r.rm_post) in + let b = f_eHoareS (snd r.rm_me) pr r.rm_framed (ehs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). A side condition that does not hold is reported as a tactic + error. *) +let t_ehoare_rmatch_framed (n : ehoare_rmatch_framed) (tc : tcenv1) = + let hs = tc1_as_ehoareS tc in + let sg = + try ehoare_rmatch_framed_subgoals (FApi.tc1_hyps tc) hs n + with InvalidTransform msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REHoareRMatchFramed n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REHoareRMatchFramed n -> + Some (EcPlRecheck.checker_of "ehoare-rmatch-framed" pf_as_ehoareS + (fun hyps hs -> ehoare_rmatch_framed_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Parameters of the ehoare [rmatch] tactic as supplied by the caller: high + level, the position and the constructor are still symbolic. *) +type ehoare_rmatch_rule = { + ehrmr_at : EcMatching.Position.codepos1; (* position of the match *) + ehrmr_ctor : EcSymbols.symbol; (* constructor of the branch *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position and the constructor + (failing as before the migration), then apply the framed rule when the + framing condition holds, the [rmatch] transformation through the ehoare + transformation rule otherwise (both check the form of the + precondition). *) +let t_ehoare_rmatch (r : ehoare_rmatch_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_ehoareS tc in + let at, j = EcPlRCond.resolve_rmatch !!tc env r.ehrmr_at r.ehrmr_ctor hs.ehs_s in + if EcPlRCond.rmatch_can_frame env ~can_frame:true at hs.ehs_s then + t_ehoare_rmatch_framed { ehrmf_at = at; ehrmf_ctor = j } tc + else + let tr = EcTrRMatch.TrRMatch { trrm_at = at; trrm_ctor = j } in + EcEHoareTransform.t_ehoare_transform { ehtr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [eHoareS]. Type the position in + its memory, then apply the tactic. *) +let process_ehoare_rmatch + (c : EcSymbols.symbol) (at : EcParsetree.pcodepos1) (tc : tcenv1) += + let at = tc1_process_codepos1 tc (None, at) in + t_ehoare_rmatch { ehrmr_at = at; ehrmr_ctor = c } tc diff --git a/src/phl/rules/ehoare/ecEHoareRMatch.mli b/src/phl/rules/ehoare/ecEHoareRMatch.mli new file mode 100644 index 000000000..664c487ae --- /dev/null +++ b/src/phl/rules/ehoare/ecEHoareRMatch.mli @@ -0,0 +1,78 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type ehoare_rmatch_framed = { + ehrmf_at : nm_codepos1; (* position k of the match (resolved) *) + ehrmf_ctor : int; (* index j of the constructor C *) +} + +(* [t_ehoare_rmatch_framed { ehrmf_at = k; ehrmf_ctor = j }] — framed form + of [match C k]. With [c = hd; i; tl], [hd = c[0..k)] and + [i = c[k] = match e with ... | C xs => b | ...], [C] its [j]-th + constructor: + + hoare [hd : P ==> exists xs, e = C xs] + ehoare [hd; b[ys/xs]; tl : (e = C ys /\ P) `|` f ==> Q] + --------------------------------------------------------- e indep. of hd + ehoare [c : P `|` f ==> Q] + + where [ys] are fresh program variables, added to the memory of the + second premise. Side conditions: [i] is a [match] with a [j]-th + constructor; the variables read by [e] are neither read nor written by + [hd]; the precondition has the form [P `|` f] (otherwise fails with "the + pre should have the form \"_ `|` _\""). + + This is not a program transformation: [e = C ys] goes to the + precondition, so the rule is stated on the whole statement (implicit + seq around the match). It is retained as a separate rule pending a + later discussion (the unframed form of [match C k] is the program + transformation [EcTrRMatch]). It is sound because [e] has the same + value before and after [hd], and because the initial memories in which + [hd] does not terminate contribute nothing to the expectation of [Q]: + in the other ones, the first premise yields [ys] with [e = C ys] + initially. + + Node: [REHoareRMatchFramed { ehrmf_at = k; ehrmf_ctor = j }]. + Checker: "ehoare-rmatch-framed" (it re-checks the side conditions). *) +val t_ehoare_rmatch_framed : ehoare_rmatch_framed -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +type ehoare_rmatch_rule = { + ehrmr_at : codepos1; (* position k of the match *) + ehrmr_ctor : symbol; (* constructor C of the branch taken *) +} + +(* [t_ehoare_rmatch { ehrmr_at = k; ehrmr_ctor = C }] — decides the match + [i = c[k]] of [ehoare [c : P `|` f ==> Q]] in favour of its [C] branch. + Resolves [k] to an index and [C] to its index [j] (failing with "invalid + split index", "the targetted instruction is not a match", "cannot find + the constructor C", in this order), then applies: + - when the variables read by [e] are neither read nor written by the + prefix [hd] (framed form): [t_ehoare_rmatch_framed { k; j }]; + - otherwise (unframed form): [EcEHoareTransform.t_ehoare_transform] + with [EcTrRMatch.TrRMatch { trrm_at = k; trrm_ctor = j }]. + Both fail with "the pre should have the form \"_ `|` _\"" when the + precondition is not of that form. + + Visible goals, in this order (those of the rule applied): + hoare [hd : P ==> exists xs, e = C xs] + ehoare [hd; b[ys/xs]; tl : (e = C ys /\ P) `|` f ==> Q] (framed) + ehoare [hd; ys <- oget (get_as_C e); b[ys/xs]; tl : P `|` f ==> Q] + (unframed) + Emits no node of its own. *) +val t_ehoare_rmatch : ehoare_rmatch_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match C k] on an [eHoareS] goal: types the position [k] in the goal's + memory and applies [t_ehoare_rmatch]. *) +val process_ehoare_rmatch : symbol -> pcodepos1 -> backward diff --git a/src/phl/rules/ehoare/ecEHoareTransform.mli b/src/phl/rules/ehoare/ecEHoareTransform.mli index 377192257..a249d8409 100644 --- a/src/phl/rules/ehoare/ecEHoareTransform.mli +++ b/src/phl/rules/ehoare/ecEHoareTransform.mli @@ -24,9 +24,6 @@ type ehoare_transform = { have the form \"_ `|` _\""). Side condition: [t] applies to [c] (otherwise fails with its message). - No catalogue entry is used on ehoare goals yet (there is no ehoare - [rndsem]). - Node: [REHoareTransform { ehtr_tr = t }]. Checker: "ehoare-transform" (it re-runs the entry on the goal's program). *) val t_ehoare_transform : ehoare_transform -> backward diff --git a/src/phl/rules/equiv/ecEquivRCond.ml b/src/phl/rules/equiv/ecEquivRCond.ml new file mode 100644 index 000000000..d86f51c98 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRCond.ml @@ -0,0 +1,35 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree + +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the (one-sided) equiv [rcond] tactic as supplied by the + caller: high level, the position is still symbolic and must be + resolved. *) +type equiv_rcond_rule = { + ercr_side : side; (* side of the conditional *) + ercr_at : EcMatching.Position.codepos1; (* position of the conditional *) + ercr_branch : bool; (* branch taken *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position on the chosen side + (failing as before the migration when it is invalid or not a + conditional) and apply the [rcond] transformation to that side through + the equiv transformation rule. *) +let t_equiv_rcond (r : equiv_rcond_rule) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let s = sideif r.ercr_side es.es_sl es.es_sr in + let at = EcPlRCond.resolve_rcond !!tc (FApi.tc1_env tc) r.ercr_at s in + let tr = EcTrRCond.TrRCond { trrc_at = at; trrc_branch = r.ercr_branch } in + EcEquivTransform.t_equiv_transform { etr_side = r.ercr_side; etr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS] (or is reported as not + being one when typing the position). Type the position in the memory of + [side], then apply the tactic. *) +let process_equiv_rcond (side : side) (b : bool) (at : pcodepos1) (tc : tcenv1) = + let at = tc1_process_codepos1 tc (Some side, at) in + t_equiv_rcond { ercr_side = side; ercr_at = at; ercr_branch = b } tc diff --git a/src/phl/rules/equiv/ecEquivRCond.mli b/src/phl/rules/equiv/ecEquivRCond.mli new file mode 100644 index 000000000..655e3a237 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRCond.mli @@ -0,0 +1,37 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Derived tactics *) + +type equiv_rcond_rule = { + ercr_side : side; (* side of the conditional *) + ercr_at : codepos1; (* position k of the conditional, on that side *) + ercr_branch : bool; (* branch b taken *) +} + +(* [t_equiv_rcond { ercr_side = `Left; ercr_at = k; ercr_branch = b }] — + decides the conditional [i = c[k]] of the left program of + [equiv [c ~ d : P ==> Q]], with [c = hd; i; tl] (symmetrically for + [`Right]). Resolves [k] to an index (failing with "invalid split index" + when it is invalid, then with "the targetted instruction is not a + conditionnal" when [i] is neither an [if] nor a [while]), then applies + + [EcEquivTransform.t_equiv_transform] on that side with + [EcTrRCond.TrRCond { trrc_at = k (resolved); trrc_branch = b }] + + Visible goals, in this order (those of the rule): + forall &2, hoare [hd : P ==> e] (b = true; [!e] when b = false) + equiv [c' ~ d : P ==> Q] + with [c'] the decided statement (see [EcTrRCond]). Emits no node of its + own. *) +val t_equiv_rcond : equiv_rcond_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rcondt{i} k] / [rcondf{i} k] on an [equivS] goal: types the position + [k] in the memory of side [i] and applies [t_equiv_rcond]. *) +val process_equiv_rcond : side -> bool -> pcodepos1 -> backward diff --git a/src/phl/rules/equiv/ecEquivRMatch.ml b/src/phl/rules/equiv/ecEquivRMatch.ml new file mode 100644 index 000000000..1eb4425a0 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRMatch.ml @@ -0,0 +1,115 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcFol +open EcAst +open EcEnv +open EcSubst + +open EcCoreGoal +open EcLowPhlGoal +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the framed (one-sided) equiv [rmatch] rule, resolved: the + position of the match and its constructor are integer indices. Nothing + to resolve: the same record is the rule argument and the node + payload. *) +type equiv_rmatch_framed = { + ermf_side : side; (* side of the match *) + ermf_at : EcMatching.Position.nm_codepos1; (* position of the match *) + ermf_ctor : int; (* index of the constructor *) +} + +type EcCoreGoal.rule += REquivRMatchFramed of equiv_rmatch_framed + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + instruction is a [match] with that constructor, the prefix is empty) + are re-checked here, from the goal: the checker re-validates them. The + prefix obligation is a hoare judgement on the side of the match, the + other memory being universally quantified, and [e = C ys] is added to + the relational precondition. *) +let equiv_rmatch_framed_subgoals + (hyps : LDecl.hyps) (es : equivS) (n : equiv_rmatch_framed) += + let env = LDecl.toenv hyps in + let side = n.ermf_side in + let m, mo, s = + match side with + | `Left -> es.es_ml, es.es_mr, es.es_sl + | `Right -> es.es_mr, es.es_ml, es.es_sr in + let r = EcPlRCond.rmatch_select env m n.ermf_at n.ermf_ctor s in + if not (EcPlRCond.rmatch_can_frame env ~can_frame:false n.ermf_at s) then + raise (InvalidTransform "the framed form of match does not apply"); + let ss_inv_generalize_other inv = + sideif side ss_inv_generalize_right ss_inv_generalize_left inv (fst mo) in + let ts_inv_lower_side1 = + sideif side ts_inv_lower_left1 ts_inv_lower_right1 in + let eq = ss_inv_generalize_other (ss_inv_rebind r.rm_eq (fst m)) in + let po = POE.lift r.rm_post in + let a = + f_forall_mems_ss_inv mo + (ts_inv_lower_side1 (fun pr -> f_hoareS (snd m) pr r.rm_hd po) (es_pr es)) in + let b = + let pr = map_ts_inv2 f_and eq (es_pr es) in + match side with + | `Left -> + f_equivS (snd r.rm_me) (snd es.es_mr) pr r.rm_framed es.es_sr (es_po es) + | `Right -> + f_equivS (snd es.es_ml) (snd r.rm_me) pr es.es_sl r.rm_framed (es_po es) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). A side condition that does not hold is reported as a tactic + error. *) +let t_equiv_rmatch_framed (n : equiv_rmatch_framed) (tc : tcenv1) = + let es = tc1_as_equivS tc in + let sg = + try equiv_rmatch_framed_subgoals (FApi.tc1_hyps tc) es n + with InvalidTransform msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (REquivRMatchFramed n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | REquivRMatchFramed n -> + Some (EcPlRecheck.checker_of "equiv-rmatch-framed" pf_as_equivS + (fun hyps es -> equiv_rmatch_framed_subgoals hyps es n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Parameters of the (one-sided) equiv [rmatch] tactic as supplied by the + caller: high level, the position and the constructor are still + symbolic. *) +type equiv_rmatch_rule = { + ermr_side : side; (* side of the match *) + ermr_at : EcMatching.Position.codepos1; (* position of the match *) + ermr_ctor : EcSymbols.symbol; (* constructor of the branch *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position and the constructor on the + chosen side (failing as before the migration), then apply the framed + rule when the prefix is empty, the [rmatch] transformation to that side + through the equiv transformation rule otherwise. *) +let t_equiv_rmatch (r : equiv_rmatch_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let es = tc1_as_equivS tc in + let s = sideif r.ermr_side es.es_sl es.es_sr in + let at, j = EcPlRCond.resolve_rmatch !!tc env r.ermr_at r.ermr_ctor s in + if EcPlRCond.rmatch_can_frame env ~can_frame:false at s then + t_equiv_rmatch_framed { ermf_side = r.ermr_side; ermf_at = at; ermf_ctor = j } tc + else + let tr = EcTrRMatch.TrRMatch { trrm_at = at; trrm_ctor = j } in + EcEquivTransform.t_equiv_transform { etr_side = r.ermr_side; etr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be an [equivS] (or is reported as not + being one when typing the position). Type the position in the memory of + [side], then apply the tactic. *) +let process_equiv_rmatch + (side : side) (c : EcSymbols.symbol) (at : pcodepos1) (tc : tcenv1) += + let at = tc1_process_codepos1 tc (Some side, at) in + t_equiv_rmatch { ermr_side = side; ermr_at = at; ermr_ctor = c } tc diff --git a/src/phl/rules/equiv/ecEquivRMatch.mli b/src/phl/rules/equiv/ecEquivRMatch.mli new file mode 100644 index 000000000..9432142a8 --- /dev/null +++ b/src/phl/rules/equiv/ecEquivRMatch.mli @@ -0,0 +1,78 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type equiv_rmatch_framed = { + ermf_side : side; (* side of the match *) + ermf_at : nm_codepos1; (* position k of the match (resolved) *) + ermf_ctor : int; (* index j of the constructor C *) +} + +(* [t_equiv_rmatch_framed { ermf_side = `Left; ermf_at = k; ermf_ctor = j }] + — framed form of [match C {1} k], on an empty prefix. With + [c = i; tl] ([k = 0]) and [i = match e with ... | C xs => b | ...], [C] + its [j]-th constructor: + + forall &2, hoare [skip : P ==> exists xs, e = C xs] + equiv [b[ys/xs]; tl ~ d : e{1} = C ys{1} /\ P ==> Q] + ------------------------------------------------------ k = 0 + equiv [c ~ d : P ==> Q] + + (symmetrically for [`Right]), where [P] is read on [&1] in the first + premise and [ys] are fresh program variables, added to the memory of + the left program in the second one. Side conditions: [i] is a [match] + with a [j]-th constructor; the prefix [c[0..k)] is empty (and so, + trivially, does not read or write [e]). + + This is not a program transformation: [e = C ys] goes to the + precondition. It is retained as a separate rule pending a later + discussion (the unframed form of [match C k] is the program + transformation [EcTrRMatch]). It is sound because the empty prefix + terminates: the first premise yields [ys] with [e = C ys] in every + initial memory satisfying [P]. With a non-empty prefix, the initial + memories in which it does not terminate would not be covered by the + second premise, which is unsound for an equiv judgement. + + Node: [REquivRMatchFramed { ermf_side; ermf_at = k; ermf_ctor = j }]. + Checker: "equiv-rmatch-framed" (it re-checks the side conditions). *) +val t_equiv_rmatch_framed : equiv_rmatch_framed -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +type equiv_rmatch_rule = { + ermr_side : side; (* side of the match *) + ermr_at : codepos1; (* position k of the match, on that side *) + ermr_ctor : symbol; (* constructor C of the branch taken *) +} + +(* [t_equiv_rmatch { ermr_side = `Left; ermr_at = k; ermr_ctor = C }] — + decides the match [i = c[k]] of the left program of + [equiv [c ~ d : P ==> Q]] in favour of its [C] branch, with + [c = hd; i; tl] (symmetrically for [`Right]). Resolves [k] to an index + and [C] to its index [j] (failing with "invalid split index", "the + targetted instruction is not a match", "cannot find the constructor C", + in this order), then applies: + - when [hd] is empty (framed form): [t_equiv_rmatch_framed]; + - otherwise (unframed form): [EcEquivTransform.t_equiv_transform] on + that side with [EcTrRMatch.TrRMatch { trrm_at = k; trrm_ctor = j }]. + + Visible goals, in this order (those of the rule applied): + forall &2, hoare [hd : P ==> exists xs, e = C xs] + equiv [b[ys/xs]; tl ~ d : e{1} = C ys{1} /\ P ==> Q] (framed) + equiv [hd; ys <- oget (get_as_C e); b[ys/xs]; tl ~ d : P ==> Q] + (unframed) + Emits no node of its own. *) +val t_equiv_rmatch : equiv_rmatch_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match C {i} k] on an [equivS] goal: types the position [k] in the + memory of side [i] and applies [t_equiv_rmatch]. *) +val process_equiv_rmatch : side -> symbol -> pcodepos1 -> backward diff --git a/src/phl/rules/hoare/ecHoareRCond.ml b/src/phl/rules/hoare/ecHoareRCond.ml new file mode 100644 index 000000000..583afcb40 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRCond.ml @@ -0,0 +1,28 @@ +(* -------------------------------------------------------------------- *) +open EcCoreGoal +open EcLowPhlGoal + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [rcond] tactic as supplied by the caller: high + level, the position is still symbolic and must be resolved. *) +type hoare_rcond_rule = { + hrcr_at : EcMatching.Position.codepos1; (* position of the conditional *) + hrcr_branch : bool; (* branch taken *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position (failing as before the + migration when it is invalid or not a conditional) and apply the + [rcond] transformation through the hoare transformation rule. *) +let t_hoare_rcond (r : hoare_rcond_rule) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let at = EcPlRCond.resolve_rcond !!tc (FApi.tc1_env tc) r.hrcr_at hs.hs_s in + let tr = EcTrRCond.TrRCond { trrc_at = at; trrc_branch = r.hrcr_branch } in + EcHoareTransform.t_hoare_transform { htr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS]. Type the position in + its memory, then apply the tactic. *) +let process_hoare_rcond (b : bool) (at : EcParsetree.pcodepos1) (tc : tcenv1) = + let at = tc1_process_codepos1 tc (None, at) in + t_hoare_rcond { hrcr_at = at; hrcr_branch = b } tc diff --git a/src/phl/rules/hoare/ecHoareRCond.mli b/src/phl/rules/hoare/ecHoareRCond.mli new file mode 100644 index 000000000..1454f8931 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRCond.mli @@ -0,0 +1,35 @@ +(* -------------------------------------------------------------------- *) +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Derived tactics *) + +type hoare_rcond_rule = { + hrcr_at : codepos1; (* position k of the conditional *) + hrcr_branch : bool; (* branch b taken *) +} + +(* [t_hoare_rcond { hrcr_at = k; hrcr_branch = b }] — decides the + conditional [i = c[k]] of [hoare [c : P ==> Q | E]], with + [c = hd; i; tl]. Resolves [k] to an index (failing with "invalid split + index" when it is invalid, then with "the targetted instruction is not a + conditionnal" when [i] is neither an [if] nor a [while]), then applies + + [EcHoareTransform.t_hoare_transform] with + [EcTrRCond.TrRCond { trrc_at = k (resolved); trrc_branch = b }] + + Visible goals, in this order (those of the rule): + hoare [hd : P ==> e | E] (b = true; [!e] when b = false) + hoare [c' : P ==> Q | E] + with [c'] the decided statement (see [EcTrRCond]). Emits no node of its + own. *) +val t_hoare_rcond : hoare_rcond_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [rcondt k] / [rcondf k] on a [hoareS] goal: types the position [k] in + the goal's memory and applies [t_hoare_rcond]. *) +val process_hoare_rcond : bool -> pcodepos1 -> backward diff --git a/src/phl/rules/hoare/ecHoareRMatch.ml b/src/phl/rules/hoare/ecHoareRMatch.ml new file mode 100644 index 000000000..3a948569a --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRMatch.ml @@ -0,0 +1,88 @@ +(* -------------------------------------------------------------------- *) +open EcFol +open EcAst +open EcEnv + +open EcCoreGoal +open EcLowPhlGoal +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the framed hoare [rmatch] rule, resolved: the position of + the match and its constructor are integer indices. Nothing to resolve: + the same record is the rule argument and the node payload. *) +type hoare_rmatch_framed = { + hrmf_at : EcMatching.Position.nm_codepos1; (* position of the match *) + hrmf_ctor : int; (* index of the constructor *) +} + +type EcCoreGoal.rule += RHoareRMatchFramed of hoare_rmatch_framed + +(* -------------------------------------------------------------------- *) +(* Pure core shared by the rule and its checker. Its side conditions (the + instruction is a [match] with that constructor, the framing condition) + are re-checked here, from the goal: the checker re-validates them. *) +let hoare_rmatch_framed_subgoals + (hyps : LDecl.hyps) (hs : sHoareS) (n : hoare_rmatch_framed) += + let env = LDecl.toenv hyps in + let r = EcPlRCond.rmatch_select env hs.hs_m n.hrmf_at n.hrmf_ctor hs.hs_s in + if not (EcPlRCond.rmatch_can_frame env ~can_frame:true n.hrmf_at hs.hs_s) then + raise (InvalidTransform "the framed form of match does not apply"); + let a = f_hoareS (snd hs.hs_m) (hs_pr hs) r.rm_hd + (update_hs_ss r.rm_post (hs_po hs)) in + let b = f_hoareS (snd r.rm_me) (map_ss_inv2 f_and r.rm_eq (hs_pr hs)) + r.rm_framed (hs_po hs) in + [a; b] + +(* -------------------------------------------------------------------- *) +(* Rule (TCB). A side condition that does not hold is reported as a tactic + error. *) +let t_hoare_rmatch_framed (n : hoare_rmatch_framed) (tc : tcenv1) = + let hs = tc1_as_hoareS tc in + let sg = + try hoare_rmatch_framed_subgoals (FApi.tc1_hyps tc) hs n + with InvalidTransform msg -> tc_error !!tc "%s" msg in + FApi.xrule1 tc (RHoareRMatchFramed n) sg + +(* -------------------------------------------------------------------- *) +let () = + register_rule_checker + (function + | RHoareRMatchFramed n -> + Some (EcPlRecheck.checker_of "hoare-rmatch-framed" pf_as_hoareS + (fun hyps hs -> hoare_rmatch_framed_subgoals hyps hs n)) + | _ -> None) + +(* -------------------------------------------------------------------- *) +(* Parameters of the hoare [rmatch] tactic as supplied by the caller: high + level, the position and the constructor are still symbolic. *) +type hoare_rmatch_rule = { + hrmr_at : EcMatching.Position.codepos1; (* position of the match *) + hrmr_ctor : EcSymbols.symbol; (* constructor of the branch *) +} + +(* -------------------------------------------------------------------- *) +(* Derived (no proof-node): resolve the position and the constructor + (failing as before the migration), then apply the framed rule when the + framing condition holds, the [rmatch] transformation through the hoare + transformation rule otherwise. *) +let t_hoare_rmatch (r : hoare_rmatch_rule) (tc : tcenv1) = + let env = FApi.tc1_env tc in + let hs = tc1_as_hoareS tc in + let at, j = EcPlRCond.resolve_rmatch !!tc env r.hrmr_at r.hrmr_ctor hs.hs_s in + if EcPlRCond.rmatch_can_frame env ~can_frame:true at hs.hs_s then + t_hoare_rmatch_framed { hrmf_at = at; hrmf_ctor = j } tc + else + let tr = EcTrRMatch.TrRMatch { trrm_at = at; trrm_ctor = j } in + EcHoareTransform.t_hoare_transform { htr_tr = tr } tc + +(* -------------------------------------------------------------------- *) +(* Elaboration: the goal is known to be a [hoareS] (or is reported as not + being one when typing the position). Type the position in its memory, + then apply the tactic. *) +let process_hoare_rmatch + (c : EcSymbols.symbol) (at : EcParsetree.pcodepos1) (tc : tcenv1) += + let at = tc1_process_codepos1 tc (None, at) in + t_hoare_rmatch { hrmr_at = at; hrmr_ctor = c } tc diff --git a/src/phl/rules/hoare/ecHoareRMatch.mli b/src/phl/rules/hoare/ecHoareRMatch.mli new file mode 100644 index 000000000..447f0bd91 --- /dev/null +++ b/src/phl/rules/hoare/ecHoareRMatch.mli @@ -0,0 +1,74 @@ +(* -------------------------------------------------------------------- *) +open EcSymbols +open EcParsetree +open EcCoreGoal.FApi +open EcMatching.Position + +(* ==================================================================== *) +(* Rules (trusted) *) + +type hoare_rmatch_framed = { + hrmf_at : nm_codepos1; (* position k of the match (resolved) *) + hrmf_ctor : int; (* index j of the constructor C *) +} + +(* [t_hoare_rmatch_framed { hrmf_at = k; hrmf_ctor = j }] — framed form of + [match C k]. With [c = hd; i; tl], [hd = c[0..k)] and + [i = c[k] = match e with ... | C xs => b | ...], [C] its [j]-th + constructor: + + hoare [hd : P ==> exists xs, e = C xs | E] + hoare [hd; b[ys/xs]; tl : e = C ys /\ P ==> Q | E] + ---------------------------------------------------- e indep. of hd + hoare [c : P ==> Q | E] + + where [E] are the exceptional postconditions of the goal and [ys] are + fresh program variables, added to the memory of the second premise. + Side conditions: [i] is a [match] with a [j]-th constructor; the + variables read by [e] are neither read nor written by [hd]. + + This is not a program transformation: [e = C ys] goes to the + precondition, so the rule is stated on the whole statement (implicit + seq around the match). It is retained as a separate rule pending a + later discussion (the unframed form of [match C k] is the program + transformation [EcTrRMatch]). It is sound because [e] has the same + value before and after [hd], and because a hoare judgement ignores the + initial memories in which [hd] does not terminate: in the other ones, + the first premise yields [ys] with [e = C ys] initially. + + Node: [RHoareRMatchFramed { hrmf_at = k; hrmf_ctor = j }]. + Checker: "hoare-rmatch-framed" (it re-checks the side conditions). *) +val t_hoare_rmatch_framed : hoare_rmatch_framed -> backward + +(* ==================================================================== *) +(* Derived tactics *) + +type hoare_rmatch_rule = { + hrmr_at : codepos1; (* position k of the match *) + hrmr_ctor : symbol; (* constructor C of the branch taken *) +} + +(* [t_hoare_rmatch { hrmr_at = k; hrmr_ctor = C }] — decides the match + [i = c[k]] of [hoare [c : P ==> Q | E]] in favour of its [C] branch. + Resolves [k] to an index and [C] to its index [j] (failing with "invalid + split index", "the targetted instruction is not a match", "cannot find + the constructor C", in this order), then applies: + - when the variables read by [e] are neither read nor written by the + prefix [hd] (framed form): [t_hoare_rmatch_framed { k; j }]; + - otherwise (unframed form): [EcHoareTransform.t_hoare_transform] with + [EcTrRMatch.TrRMatch { trrm_at = k; trrm_ctor = j }]. + + Visible goals, in this order (those of the rule applied): + hoare [hd : P ==> exists xs, e = C xs | E] + hoare [hd; b[ys/xs]; tl : e = C ys /\ P ==> Q | E] (framed) + hoare [hd; ys <- oget (get_as_C e); b[ys/xs]; tl : P ==> Q | E] + (unframed) + Emits no node of its own. *) +val t_hoare_rmatch : hoare_rmatch_rule -> backward + +(* ==================================================================== *) +(* Elaboration *) + +(* [match C k] on a [hoareS] goal: types the position [k] in the goal's + memory and applies [t_hoare_rmatch]. *) +val process_hoare_rmatch : symbol -> pcodepos1 -> backward diff --git a/src/phl/rules/transforms/ecTrRCond.ml b/src/phl/rules/transforms/ecTrRCond.ml new file mode 100644 index 000000000..3e829e518 --- /dev/null +++ b/src/phl/rules/transforms/ecTrRCond.ml @@ -0,0 +1,28 @@ +(* -------------------------------------------------------------------- *) +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the [rcond] transformation, resolved: the position of the + conditional is an integer index. *) +type tr_rcond = { + trrc_at : EcMatching.Position.nm_codepos1; + trrc_branch : bool; +} + +type EcPlTransform.transform += TrRCond of tr_rcond + +(* -------------------------------------------------------------------- *) +(* Decide the conditional at index [k] in favour of the branch [b]; the + prefix must establish the corresponding guard. *) +let rcond (p : tr_rcond) (ctxt : tr_ctxt) (s : EcModules.stmt) = + let hd, g, s = + EcPlRCond.rcond_select + (EcMemory.memory ctxt.trc_me) p.trrc_at p.trrc_branch s in + { trr_me = ctxt.trc_me; + trr_s = s; + trr_obl = [OPrefixPost { opp_prefix = hd; opp_cond = g; }]; } + +let () = + register (function + | TrRCond p -> Some (rcond p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrRCond.mli b/src/phl/rules/transforms/ecTrRCond.mli new file mode 100644 index 000000000..2c1d545c0 --- /dev/null +++ b/src/phl/rules/transforms/ecTrRCond.mli @@ -0,0 +1,26 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_rcond = { + trrc_at : nm_codepos1; (* position k of the conditional (resolved) *) + trrc_branch : bool; (* branch b taken *) +} + +(* [TrRCond { trrc_at = k; trrc_branch = b }] — decides the conditional + [i = c[k]] in favour of the branch [b], with [c = hd; i; tl] and + [hd = c[0..k)]: + + c = hd; if e then c1 else c2; tl ~~> c' = hd; c1; tl (b = true) + c' = hd; c2; tl (b = false) + c = hd; while e do c1; tl ~~> c' = hd; c1; while e do c1; tl + (b = true) + c' = hd; tl (b = false) + + One obligation: [OPrefixPost (hd, e)] (b = true), [OPrefixPost (hd, !e)] + (b = false), [e] read in the memory of [c]. Same memory. Fails with "the + targetted instruction is not a conditionnal" when [i] is neither an [if] + nor a [while] (see [EcPlRCond.rcond_select]). *) +type EcPlTransform.transform += TrRCond of tr_rcond diff --git a/src/phl/rules/transforms/ecTrRMatch.ml b/src/phl/rules/transforms/ecTrRMatch.ml new file mode 100644 index 000000000..ece39a004 --- /dev/null +++ b/src/phl/rules/transforms/ecTrRMatch.ml @@ -0,0 +1,30 @@ +(* -------------------------------------------------------------------- *) +open EcModules +open EcPlTransform + +(* -------------------------------------------------------------------- *) +(* Parameters of the [rmatch] transformation, resolved: the position of + the match and its constructor are integer indices. *) +type tr_rmatch = { + trrm_at : EcMatching.Position.nm_codepos1; + trrm_ctor : int; +} + +type EcPlTransform.transform += TrRMatch of tr_rmatch + +(* -------------------------------------------------------------------- *) +(* Decide the match at index [k] in favour of its [j]-th constructor, its + arguments being assigned to fresh program variables; the prefix must + establish that constructor. *) +let rmatch (p : tr_rmatch) (ctxt : tr_ctxt) (s : stmt) = + let r = + EcPlRCond.rmatch_select + ctxt.trc_env ctxt.trc_me p.trrm_at p.trrm_ctor s in + { trr_me = r.rm_me; + trr_s = r.rm_unframed; + trr_obl = [OPrefixPost { opp_prefix = r.rm_hd; opp_cond = r.rm_post; }]; } + +let () = + register (function + | TrRMatch p -> Some (rmatch p) + | _ -> None) diff --git a/src/phl/rules/transforms/ecTrRMatch.mli b/src/phl/rules/transforms/ecTrRMatch.mli new file mode 100644 index 000000000..25697a95e --- /dev/null +++ b/src/phl/rules/transforms/ecTrRMatch.mli @@ -0,0 +1,27 @@ +(* -------------------------------------------------------------------- *) +open EcMatching.Position + +(* ==================================================================== *) +(* Catalogue entry (trusted) *) + +type tr_rmatch = { + trrm_at : nm_codepos1; (* position k of the match (resolved) *) + trrm_ctor : int; (* index j of the constructor C *) +} + +(* [TrRMatch { trrm_at = k; trrm_ctor = j }] — decides the match + [i = c[k] = match e with ... | C xs => b | ...] in favour of its [j]-th + constructor [C], with [c = hd; i; tl] and [hd = c[0..k)]: + + c = hd; i; tl ~~> c' = hd; ys <- oget (get_as_C e); b[ys/xs]; tl + + where [ys] are fresh program variables, added to the memory (no + assignment when [C] has no argument). One obligation: + [OPrefixPost (hd, exists xs, e = C xs)], in the memory of [c]. Fails + with "the targetted instruction is not a match" when [i] is not a + [match], "invalid constructor index" when it has no [j]-th branch (see + [EcPlRCond.rmatch_select]). + + This is the unframed form of [match C k]; its framed form changes the + precondition, and is a rule of each logic ([EcRMatch]). *) +type EcPlTransform.transform += TrRMatch of tr_rmatch diff --git a/tests/rcond.ec b/tests/rcond.ec new file mode 100644 index 000000000..84fe48f59 --- /dev/null +++ b/tests/rcond.ec @@ -0,0 +1,329 @@ +require import AllCore Xreal. + +(* rcondt / rcondf and match C k in every logic: the conditional (if, + while) or the match decided at a position, the prefix establishing the + branch taken. *) + +exception e1. + +module M = { + var x : int + var o : int option + + proc f(y : int) = { + var z; + z <- y; + if (z = 0) { x <- 1; } else { x <- 2; } + while (z < 1) { z <- z + 1; } + } + + proc k(y : int) = { + var z; + z <- y; + if (z = 0) { x <- 1; } else { x <- 2; } + } + + proc r(y : int) = { + var z; + x <- 0; + z <- y; + if (z = 0) { raise e1; } + x <- 1; + } + + (* The prefix neither reads nor writes [o]: framed form of [match] + (when the logic allows it). *) + proc g() = { + x <- 0; + match o with + | None => { x <- 1; } + | Some v => { x <- v; } + end; + } + + (* The prefix writes [o]: unframed form of [match]. *) + proc h() = { + o <- Some 3; + match o with + | None => { x <- 1; } + | Some v => { x <- v; } + end; + } + + (* Empty prefix: framed form of [match] in every logic. *) + proc m() = { + match o with + | None => { x <- 1; } + | Some v => { x <- v; } + end; + } +}. + +(* -------------------------------------------------------------------- *) +(* rcondt / rcondf, on an [if] and on a [while]. *) + +lemma hoare_rcondt : hoare [M.f : y = 0 ==> M.x = 1]. +proof. +proc. +rcondt 2; 1: by auto. +rcondt 3; 1: by auto. +rcondf 4; 1: by auto. +by auto. +qed. + +lemma hoare_rcondf : hoare [M.f : y <> 0 ==> M.x = 2]. +proof. +proc. +rcondf 2; 1: by auto. +by while (M.x = 2); auto. +qed. + +(* The exceptional postcondition is kept in the prefix obligation. *) +lemma hoare_rcond_exn : hoare [M.r : y = 0 ==> false | e1 => M.x = 0]. +proof. +proc. +rcondt 3; 1: by auto. +by auto. +qed. + +lemma ehoare_rcondt : ehoare [M.k : (y = 0) `|` 1%xr ==> 1%xr]. +proof. +proc. +rcondt 2; 1: by auto. +by wp; skip => &hr /#. +qed. + +lemma ehoare_rcondf : ehoare [M.f : (0 < y) `|` 1%xr ==> 1%xr]. +proof. +proc. +rcondf 2; 1: by auto => /#. +rcondf 3; 1: by wp; skip => /#. +by wp; skip => &hr /#. +qed. + +lemma phoare_rcondt : phoare [M.f : y = 0 ==> M.x = 1] = 1%r. +proof. +proc. +rcondt 2; 1: by auto. +rcondt 3; 1: by auto. +rcondf 4; 1: by auto. +by auto. +qed. + +lemma phoare_rcondf : phoare [M.k : y <> 0 ==> M.x = 2] >= 1%r. +proof. +proc. +rcondf 2; 1: by auto. +by auto. +qed. + +lemma equiv_rcond : equiv [M.f ~ M.f : y{1} = 0 /\ y{2} = 0 ==> ={M.x}]. +proof. +proc. +rcondt {1} 2; 1: by auto. +rcondt {2} 2; 1: by auto. +rcondt {1} 3; 1: by auto. +rcondf {1} 4; 1: by auto. +rcondt {2} 3; 1: by auto. +rcondf {2} 4; 1: by auto. +by auto. +qed. + +lemma equiv_rcondf : equiv [M.k ~ M.k : y{1} <> 0 /\ y{2} <> 0 ==> ={M.x}]. +proof. +proc. +rcondf {1} 2; 1: by move=> &2; auto. +rcondf {2} 2; 1: by move=> &1; auto. +by auto. +qed. + +(* -------------------------------------------------------------------- *) +(* rcond: error paths. *) + +lemma hoare_rcond_errors : hoare [M.f : y = 0 ==> M.x = 1]. +proof. +proc. +fail rcondt 1. (* not a conditional *) +fail rcondt 10. (* no such position *) +fail rcondt {1} 2. (* side on a hoare goal *) +abort. + +lemma ehoare_rcond_errors : ehoare [M.k : 1%xr ==> 1%xr]. +proof. +proc. +fail rcondt 2. (* the pre is not of the form _ `|` _ *) +fail rcondt 1. (* not a conditional *) +fail rcondf 10. (* no such position *) +abort. + +lemma phoare_rcond_errors : phoare [M.k : true ==> true] = 1%r. +proof. +proc. +fail rcondt 1. (* not a conditional *) +fail rcondt {2} 2. (* side on a phoare goal *) +abort. + +lemma equiv_rcond_errors : equiv [M.f ~ M.f : true ==> true]. +proof. +proc. +fail rcondt 2. (* no side on an equiv goal *) +fail rcondt {1} 1. (* not a conditional *) +fail rcondf {2} 10. (* no such position *) +abort. + +(* -------------------------------------------------------------------- *) +(* rmatch: framed and unframed forms. *) + +lemma hoare_rmatch_framed : hoare [M.g : M.o = Some 2 ==> M.x = 2]. +proof. +proc. +match Some 2; 1: by auto => /#. +by auto => /#. +qed. + +lemma hoare_rmatch_unframed : hoare [M.h : true ==> M.x = 3]. +proof. +proc. +match Some 2; 1: by auto => /#. +by auto. +qed. + +lemma hoare_rmatch_none : hoare [M.g : M.o = None ==> M.x = 1]. +proof. +proc. +match None 2; 1: by auto. +by auto. +qed. + +lemma ehoare_rmatch_framed : + ehoare [M.g : (M.o = Some 2) `|` 1%xr ==> (M.x = 2)%xr]. +proof. +proc. +match Some 2; 1: by auto => /#. +by wp; skip => &hr /#. +qed. + +lemma ehoare_rmatch_unframed : ehoare [M.h : true `|` 1%xr ==> (M.x = 3)%xr]. +proof. +proc. +match Some 2; 1: by auto => /#. +by wp; skip => &hr /#. +qed. + +lemma phoare_le_rmatch_framed : phoare [M.g : M.o = Some 2 ==> M.x = 2] <= 1%r. +proof. +proc. +match Some 2; 1: by auto => /#. +by auto => /#. +qed. + +(* phoare = with a non-empty prefix: unframed form. *) +lemma phoare_eq_rmatch_unframed : phoare [M.g : M.o = Some 2 ==> M.x = 2] = 1%r. +proof. +proc. +match Some 2; 1: by auto => /#. +by auto => /#. +qed. + +lemma phoare_rmatch_unframed : phoare [M.h : true ==> M.x = 3] = 1%r. +proof. +proc. +match Some 2; 1: by auto => /#. +by auto. +qed. + +lemma phoare_ge_rmatch_empty_framed : phoare [M.m : M.o = Some 2 ==> M.x = 2] >= 1%r. +proof. +proc. +match Some 1; 1: by auto => /#. +by auto => /#. +qed. + +(* equiv with a non-empty prefix: unframed form, on both sides. *) +lemma equiv_rmatch : equiv [M.g ~ M.h : M.o{1} = Some 3 ==> ={M.x}]. +proof. +proc. +match Some {1} 2; 1: by move=> &2; auto => /#. +match Some {2} 2; 1: by move=> &1; auto => /#. +by auto => /#. +qed. + +lemma equiv_rmatch_sym : equiv [M.h ~ M.g : M.o{2} = Some 3 ==> ={M.x}]. +proof. +proc. +match Some {2} 2; 1: by auto => /#. +match Some {1} 2; 1: by auto => /#. +by auto => /#. +qed. + +(* equiv with an empty prefix: framed form, on both sides. *) +lemma equiv_rmatch_empty_framed : + equiv [M.m ~ M.m : ={M.o} /\ M.o{1} = Some 3 ==> ={M.x}]. +proof. +proc. +match Some {1} 1; 1: by move=> &2; auto => /#. +match Some {2} 1; 1: by move=> &1; auto => /#. +by auto => /#. +qed. + +(* The plain [match] tactic goes through the framed rule (empty prefix). *) +lemma hoare_match : hoare [M.m : true ==> true]. +proof. +proc. +match. ++ by auto. ++ by auto. +qed. + +lemma equiv_match : equiv [M.m ~ M.m : ={M.o} ==> ={M.x}]. +proof. +proc. +match {1}. ++ match {2}; 1: by auto. + by exfalso => /#. ++ match {2}; 2: by auto. + by exfalso => /#. +qed. + +(* -------------------------------------------------------------------- *) +(* rmatch: error paths. *) + +lemma hoare_rmatch_errors : hoare [M.g : true ==> true]. +proof. +proc. +fail match Some 1. (* not a match *) +fail match Foo 2. (* no such constructor *) +fail match Some 10. (* no such position *) +fail match Some {1} 2. (* side on a hoare goal *) +abort. + +lemma ehoare_rmatch_errors : ehoare [M.g : 1%xr ==> 1%xr]. +proof. +proc. +fail match Some 2. (* the pre is not of the form _ `|` _ (framed) *) +fail match Some 1. (* not a match *) +fail match Foo 2. (* no such constructor *) +abort. + +lemma ehoare_rmatch_errors_unframed : ehoare [M.h : 1%xr ==> 1%xr]. +proof. +proc. +fail match Some 2. (* the pre is not of the form _ `|` _ (unframed) *) +abort. + +lemma phoare_rmatch_errors : phoare [M.g : true ==> true] <= 1%r. +proof. +proc. +fail match Some 1. (* not a match *) +fail match Foo 2. (* no such constructor *) +fail match Some 10. (* no such position *) +abort. + +lemma equiv_rmatch_errors : equiv [M.g ~ M.h : true ==> true]. +proof. +proc. +fail match Some 2. (* no side on an equiv goal *) +fail match Some {1} 1. (* not a match *) +fail match Foo {2} 2. (* no such constructor *) +fail match Some {2} 9. (* no such position *) +abort.