From affccbdcd7c0f75fc76270a4c11e8afe9174d26e Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Fri, 4 Sep 2026 15:54:25 +0200 Subject: [PATCH] feat(phl): `proc rewrite` over ranges and whole statements `proc rewrite` used to act on exactly one instruction per invocation, so normalising the constants of a cloned procedure body took one call per statement, with hand-computed positions for nested branches. The position is now optional and may be a range: proc rewrite {2} 3 /= (* one instruction, deep *) proc rewrite {2} [2..11] /= (* a range, deep *) proc rewrite {2} /= (* the whole program, deep *) proc rewrite {2} ^while.1?:[1..1] addzC All forms recurse into the bodies of if/while/match and apply the rewrite to every expression (assignment and sampling right-hand sides, guards, call arguments, raise). In lemma mode, instructions without an occurrence of the pattern are skipped; the tactic fails only if nothing was rewritten. One side goal is emitted per rewritten expression and all are discharged internally. A single position is the singleton range. This changes the behaviour of lemma rewrites at an if/while/match position, which used to touch the guard only; they now also rewrite one occurrence in every body expression. Match-arm binders are in scope for the rewrite and are renamed apart from the proof context in the side goals, so a lemma local sharing a binder's name does not clash. The position-less lemma form takes a proof term without a leading `@' so that `proc rewrite at' stays unambiguous. `i_map_expr` is now derived from a new `i_fold_map_expr` that threads an accumulator and the match-arm locals in scope. The single-expression `t_change` is subsumed by the range version; its only caller, the expression form of `proc change`, was unreachable from the grammar and is removed. --- src/ecCoreModules.ml | 70 +++++++--- src/ecCoreModules.mli | 13 ++ src/ecParser.mly | 9 +- src/ecParsetree.ml | 2 +- src/phl/ecPhlRewrite.ml | 215 ++++++++++++++++++----------- src/phl/ecPhlRewrite.mli | 7 +- tests/procrewrite-block.ec | 270 +++++++++++++++++++++++++++++++++++++ 7 files changed, 484 insertions(+), 102 deletions(-) create mode 100644 tests/procrewrite-block.ec diff --git a/src/ecCoreModules.ml b/src/ecCoreModules.ml index eb202d64e..427509118 100644 --- a/src/ecCoreModules.ml +++ b/src/ecCoreModules.ml @@ -200,22 +200,60 @@ let i_iter (f : instr -> unit) = in fun (i : instr) -> i_iter i (* -------------------------------------------------------------------- *) -let i_map_expr (tx : expr -> expr) = - let rec doit (i : instr) = - match i.i_node with - | Sasgn (lv, e) -> i_asgn (lv, (tx e)) - | Sif (c, t, f) -> i_if (tx c, doit_s t, doit_s f) - | Smatch (e, cs) -> i_match (tx e, List.map (snd_map doit_s) cs) - | Swhile (c, bd) -> i_while (tx c, doit_s bd) - | Srnd (lv, e) -> i_rnd (lv, tx e) - | Sraise e -> i_raise (tx e) - | Sabstract (_ : memory) -> i - | Scall (lv, f, args) -> i_call (lv, f, List.map tx args) - - and doit_s (s : stmt) = - stmt (List.map doit s.s_node) in - - fun i -> doit i +let rec i_fold_map_expr + ?(locals : (EcIdent.t * ty) list = []) + (tx : (EcIdent.t * ty) list -> 'a -> expr -> 'a * expr) + (acc : 'a) + (i : instr) += + let tx1 = tx locals in + let txs = s_fold_map_expr ~locals tx in + + match i.i_node with + | Sasgn (lv, e) -> + let acc, e = tx1 acc e in + acc, i_asgn (lv, e) + + | Srnd (lv, e) -> + let acc, e = tx1 acc e in + acc, i_rnd (lv, e) + + | Scall (lv, f, args) -> + let acc, args = List.fold_left_map tx1 acc args in + acc, i_call (lv, f, args) + + | Sif (c, t, f) -> + let acc, c = tx1 acc c in + let acc, t = txs acc t in + let acc, f = txs acc f in + acc, i_if (c, t, f) + + | Swhile (c, bd) -> + let acc, c = tx1 acc c in + let acc, bd = txs acc bd in + acc, i_while (c, bd) + + | Smatch (e, bs) -> + let acc, e = tx1 acc e in + let acc, bs = + List.fold_left_map (fun acc (xs, s) -> + let acc, s = s_fold_map_expr ~locals:(locals @ xs) tx acc s in + acc, (xs, s)) acc bs in + acc, i_match (e, bs) + + | Sraise e -> + let acc, e = tx1 acc e in + acc, i_raise e + + | Sabstract (_ : memory) -> + acc, i + +and s_fold_map_expr ?(locals = []) tx acc (s : stmt) = + let acc, is = List.fold_left_map (i_fold_map_expr ~locals tx) acc s.s_node in + acc, stmt is + +let i_map_expr (tx : expr -> expr) (i : instr) = + snd (i_fold_map_expr (fun _ () e -> (), tx e) () i) (* -------------------------------------------------------------------- *) module Uninit = struct (* FIXME: generalize this for use in ecPV *) diff --git a/src/ecCoreModules.mli b/src/ecCoreModules.mli index 060fc4756..0ba1b941f 100644 --- a/src/ecCoreModules.mli +++ b/src/ecCoreModules.mli @@ -84,6 +84,19 @@ val i_asgn_of_pve : ((prog_var * ty) * expr) list -> instr option val i_iter : (instr -> unit) -> instr -> unit val i_map_expr : (expr -> expr) -> instr -> instr +(* Fold-map over the expressions of an instruction in program order, + recursing into the bodies of [if]/[while]/[match]. The callback + receives the match-arm locals in scope (on top of [locals]). *) +val i_fold_map_expr : + ?locals:(EcIdent.t * ty) list + -> ((EcIdent.t * ty) list -> 'a -> expr -> 'a * expr) + -> 'a -> instr -> 'a * instr + +val s_fold_map_expr : + ?locals:(EcIdent.t * ty) list + -> ((EcIdent.t * ty) list -> 'a -> expr -> 'a * expr) + -> 'a -> stmt -> 'a * stmt + (* -------------------------------------------------------------------- *) val get_uninit_read : stmt -> Sx.t diff --git a/src/ecParser.mly b/src/ecParser.mly index 71c883eba..9b180e226 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -3396,10 +3396,13 @@ direction: | PROC CHANGE side=side? pos=codegap COLON b=option(bracket(ptybindings)) s=brace(stmt) { Pchangestmt (side, b, Gap pos, s) } -| PROC REWRITE side=side? pos=codepos f=pterm - { Pprocrewrite (side, pos, `Rw f) } +| PROC REWRITE side=side? pos=codepos_or_range f=pterm + { Pprocrewrite (side, Some pos, `Rw f) } -| PROC REWRITE side=side? pos=codepos SLASHEQ +| PROC REWRITE side=side? f=gpterm(form_h?) + { Pprocrewrite (side, None, `Rw f) } + +| PROC REWRITE side=side? pos=codepos_or_range? SLASHEQ { Pprocrewrite (side, pos, `Simpl) } | PROC REWRITE AT tg=ident f=pterm diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 40f3656e7..b4a7ab105 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -902,7 +902,7 @@ type phltactic = | Prw_equiv of rw_eqv_info | Psymmetry | Pbdhoare_split of bdh_split - | Pprocrewrite of side option * pcodepos * prrewrite + | Pprocrewrite of side option * pcodepos_or_range option * prrewrite | Pprocrewriteat of psymbol * ppterm | Pchangestmt of side option * ptybindings option * prange1_or_insert * pstmt | Phoaresplit diff --git a/src/phl/ecPhlRewrite.ml b/src/phl/ecPhlRewrite.ml index 372edeb39..3eee837d6 100644 --- a/src/phl/ecPhlRewrite.ml +++ b/src/phl/ecPhlRewrite.ml @@ -11,31 +11,24 @@ module L = EcLocation module PT = EcProofTerm (* -------------------------------------------------------------------- *) -let t_change - (side : side option) - (pos : EcMatching.Position.codepos) - (expr : expr -> LDecl.hyps * memenv -> 'a * expr) - (tc : tcenv1) +(* [t_change_range side range expr tc] applies [expr] to every expression + of the instructions selected by [range] (the whole statement when + [range] is [None]), recursing into the bodies of [if]/[while]/[match]. + [expr] receives the hypotheses extended with the match-arm locals in + scope and returns [None] to leave an expression untouched. + + One equality side goal is emitted per rewritten expression, in program + order, followed by the rewritten program-logic goal. Each side goal is + of the form [forall &m, forall locals, e = e'] and is returned along + with the identifiers to introduce to reach the equality. *) +let t_change_range + (side : side option) + (range : EcMatching.Position.codegap_range option) + (expr : expr -> LDecl.hyps * memenv -> ('a * expr) option) + (tc : tcenv1) = let hyps, concl = FApi.tc1_flat tc in - - let change (m : memenv) (i : instr) = - let e, _, mk = - EcUtils.ofdfl - (fun () -> - tc_error !!tc - "targetted instruction should contain an expression") - (get_expression_of_instruction i) - in - - let data, e' = expr e (hyps, m) in - let mid = EcMemory.memory m in - - let f = ss_inv_of_expr mid e in - let f' = ss_inv_of_expr mid e' in - - (data, [EcSubst.f_forall_mems_ss_inv m (map_ss_inv2 f_eq f f')]), [mk e'] - in + let env = FApi.tc1_env tc in let kinds = [`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt] in @@ -45,30 +38,76 @@ let t_change (hoare | ehoare | phoare | equiv)"; let m, s = EcLowPhlGoal.tc1_get_stmt side tc in - let (data, goals), s = - EcMatching.Zipper.map (FApi.tc1_env tc) pos (change m) s in - let concl = EcLowPhlGoal.hl_set_stmt side concl s in + let mid = EcMemory.memory m in + + (* Match-arm locals are renamed apart from the hypotheses for the side + goal; the program keeps its own binders. *) + let change (locals : (EcIdent.t * ty) list) acc (e : expr) = + let ids = + LDecl.fresh_ids hyps (List.map (fun (x, _) -> EcIdent.name x) locals) in + let fresh = List.map2 (fun id (_, ty) -> (id, ty)) ids locals in + let hyps = + List.fold_left + (fun hyps (id, ty) -> LDecl.add_local id (LD_var (ty, None)) hyps) + hyps fresh in + + let rename (froms : (EcIdent.t * ty) list) (tos : (EcIdent.t * ty) list) = + let subst = + List.fold_left2 + (fun subst (x, _) (y, ty) -> + EcCoreSubst.bind_elocal subst x (EcTypes.e_local y ty)) + EcCoreSubst.Fsubst.f_subst_id froms tos + in EcCoreSubst.e_subst subst in + + let e = rename locals fresh e in + + match expr e (hyps, m) with + | None -> + acc, rename fresh locals e + + | Some (data, e') -> + let f = ss_inv_of_expr mid e in + let f' = ss_inv_of_expr mid e' in + let goal = map_ss_inv2 f_eq f f' in + let goal = + map_ss_inv1 + (f_forall (List.map (fun (x, ty) -> (x, GTty ty)) fresh)) + goal in + let goal = EcSubst.f_forall_mems_ss_inv m goal in + ((data, mid :: ids), goal) :: acc, rename fresh locals e' + in - data, FApi.xmutate1 tc `ProcChange (goals @ [concl]) + let rec locals_of_path (path : EcMatching.Zipper.ipath) = + match path with + | ZTop -> [] + | ZWhile (_, (_, path)) + | ZIfThen (_, (_, path), _) + | ZIfElse (_, _, (_, path)) -> locals_of_path path + | ZMatch (_, (_, path), ctxt) -> locals_of_path path @ ctxt.locals + in -(* -------------------------------------------------------------------- *) -let process_change - (side : side option) - (pos : pcodepos) - (form : pexpr) - (tc : tcenv1) -= - let pos = EcLowPhlGoal.tc1_process_codepos tc (side, pos) in - - let expr (e : expr) ((hyps, m) : LDecl.hyps * memenv) = - let hyps = LDecl.push_active_ss m hyps in - let e = - EcProofTyping.pf_process_exp - !!tc hyps `InProc (Some e.e_ty) form - in (), e + let acc, s = + match range with + | None -> + s_fold_map_expr change [] s + + | Some range -> + let zpr, (_, body, epilog), _ = + try + EcMatching.Zipper.zipper_and_split_of_cgap_range env range s + with EcMatching.Position.InvalidCPos -> + tc_error !!tc "invalid code position" + in + let locals = locals_of_path zpr.z_path in + let acc, body = + List.fold_left_map (i_fold_map_expr ~locals change) [] body in + acc, EcMatching.Zipper.zip { zpr with z_tail = body @ epilog } in - let (), tc = t_change side pos expr tc in tc + let data, goals = List.split (List.rev acc) in + let concl = EcLowPhlGoal.hl_set_stmt side concl s in + + data, FApi.xmutate1 tc `ProcChange (goals @ [concl]) (* -------------------------------------------------------------------- *) let try_rewrite_patterns @@ -102,74 +141,94 @@ let try_rewrite_patterns in List.find_map_opt try1 pts +(* -------------------------------------------------------------------- *) +let tc1_process_range + (tc : tcenv1) + (side : side option) + (pos : pcodepos_or_range option) += + Option.map + (fun pos -> EcLowPhlGoal.tc1_process_codepos_or_range tc (side, pos)) + pos + (* -------------------------------------------------------------------- *) let process_rewrite_rw (side : side option) - (pos : pcodepos) + (pos : pcodepos_or_range option) (pt : ppterm) (tc : tcenv1) = let hyps = FApi.tc1_hyps tc in - let ptenv = EcProofTerm.ptenv_of_penv hyps !!tc in - let pt = EcProofTerm.process_full_pterm ptenv pt in - - let pts = EcHiGoal.LowRewrite.find_rewrite_patterns `LtoR pt in - let change (e : expr) ((hyps, m) : LDecl.hyps * memenv) = - let e = form_of_expr ~m:(fst m) e in - - let data, e = - EcUtils.ofdfl - (fun () -> tc_error !!tc "cannot find a pattern to rewrite") - (try_rewrite_patterns hyps pts e) in - - (m, data), (expr_of_ss_inv { m = fst m; inv = e; }) - in - - let pos = EcLowPhlGoal.tc1_process_codepos tc (side, pos) in - let (m, (pt, mode, cpos)), tc = t_change side pos change tc in - let cpos = EcMatching.FPosition.reroot [1] cpos in - - let discharge (tc : tcenv1) = - let tc = EcLowGoal.t_intros_i_1 [fst m] tc in + (* Each expression gets its own instance of the proof term, so that the + pattern variables can be instantiated independently. *) + let patterns (hyps : LDecl.hyps) = + let ptenv = EcProofTerm.ptenv_of_penv hyps !!tc in + let pt = EcProofTerm.process_full_pterm ptenv pt in + EcHiGoal.LowRewrite.find_rewrite_patterns `LtoR pt in + + let change (hyps : LDecl.hyps) (m : memenv) (e : expr) = + let f = form_of_expr ~m:(fst m) e in + try_rewrite_patterns hyps (patterns hyps) f + |> Option.map (fun (data, f) -> + data, expr_of_ss_inv { m = fst m; inv = f; }) in + + let discharge ((pt, mode, cpos), ids) (tc : tcenv1) = + let cpos = EcMatching.FPosition.reroot [1] cpos in + let tc = EcLowGoal.t_intros_i_1 ids tc in FApi.t_seq (EcLowGoal.t_rewrite ~mode pt (`LtoR, Some cpos)) EcLowGoal.t_reflex tc in - FApi.t_first discharge tc + (* Fail early on an ill-formed proof term, even if no expression gets + rewritten. *) + ignore (patterns hyps : _ list); + + let range = tc1_process_range tc side pos in + + let change (e : expr) ((hyps, m) : LDecl.hyps * memenv) = + change hyps m e in + + let data, tce = t_change_range side range change tc in + + if List.is_empty data then + tc_error !!tc "cannot find a pattern to rewrite"; + + FApi.t_sub (List.map discharge data @ [EcLowGoal.t_id]) tce (* -------------------------------------------------------------------- *) let process_rewrite_simpl (side : side option) - (pos : pcodepos) + (pos : pcodepos_or_range option) (tc : tcenv1) = -let ri = EcReduction.nodelta in + let ri = EcReduction.nodelta in -let change (e : expr) ((hyps, me) : LDecl.hyps * memenv) = + let change (e : expr) ((hyps, me) : LDecl.hyps * memenv) = let f = ss_inv_of_expr (fst me) e in let f = map_ss_inv1 (EcCallbyValue.norm_cbv ri hyps) f in - let e = expr_of_ss_inv f in - (fst me, f), e + let e' = expr_of_ss_inv f in + if e_equal e e' then None else Some (f, e') in - let pos = EcLowPhlGoal.tc1_process_codepos tc (side, pos) in - let (m, f), tc = t_change side pos change tc in - - FApi.t_first ( + let discharge (f, ids) = FApi.t_seqs [ - EcLowGoal.t_intro_s (`Ident m); + EcLowGoal.t_intros_i ids; EcLowGoal.t_change ~ri (map_ss_inv2 f_eq f f).inv; EcLowGoal.t_reflex ] - ) tc + in + + let range = tc1_process_range tc side pos in + let data, tc = t_change_range side range change tc in + FApi.t_sub (List.map discharge data @ [EcLowGoal.t_id]) tc (* -------------------------------------------------------------------- *) let process_rewrite (side : side option) - (pos : pcodepos) + (pos : pcodepos_or_range option) (rw : prrewrite) (tc : tcenv1) = diff --git a/src/phl/ecPhlRewrite.mli b/src/phl/ecPhlRewrite.mli index ec2453f37..6a8051702 100644 --- a/src/phl/ecPhlRewrite.mli +++ b/src/phl/ecPhlRewrite.mli @@ -3,9 +3,8 @@ open EcParsetree open EcCoreGoal.FApi (* -------------------------------------------------------------------- *) -val process_change : side option -> pcodepos -> pexpr -> backward -val process_rewrite_rw : side option -> pcodepos -> ppterm -> backward -val process_rewrite_simpl : side option -> pcodepos -> backward -val process_rewrite : side option -> pcodepos -> prrewrite -> backward +val process_rewrite_rw : side option -> pcodepos_or_range option -> ppterm -> backward +val process_rewrite_simpl : side option -> pcodepos_or_range option -> backward +val process_rewrite : side option -> pcodepos_or_range option -> prrewrite -> backward val process_rewrite_at : psymbol -> ppterm -> backward val process_change_stmt : side option -> ptybindings option -> prange1_or_insert -> pstmt -> backward diff --git a/tests/procrewrite-block.ec b/tests/procrewrite-block.ec new file mode 100644 index 000000000..3c78aa095 --- /dev/null +++ b/tests/procrewrite-block.ec @@ -0,0 +1,270 @@ +(* Tests for `proc rewrite` over positions, ranges and whole statements: + the rewrite recurses into the bodies of if/while/match and applies to + every expression of the selected instructions. *) + +require import AllCore Distr. + +op foo : int -> int. +op bar : int -> int. + +axiom fooE (x : int) : foo x = x + 1. +axiom barE (x : int) : bar x = x * 2. + +hint simplify fooE, barE. + +(* -------------------------------------------------------------------- *) +(* Whole body, `/=` mode: guards, right-hand sides, then- and + else-branches, sampling and call arguments are all normalised. *) +theory BlockSimpl. + module M = { + proc h(y : int) : int = { + return y; + } + + proc f(a : int, b : int) : int = { + var c, i, d : int; + + c <- foo a; + i <- 0; + while (i < bar b) { + if (foo i = 0) { + c <- c + foo i; + } else { + c <- c + bar i; + } + i <- i + 1; + } + d <$ dunit (foo c); + c <@ h(bar d); + return c; + } + + proc g(a : int, b : int) : int = { + var c, i, d : int; + + c <- a + 1; + i <- 0; + while (i < b * 2) { + if (i + 1 = 0) { + c <- c + (i + 1); + } else { + c <- c + i * 2; + } + i <- i + 1; + } + d <$ dunit (c + 1); + c <@ h(d * 2); + return c; + } + }. + + lemma L : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} /=. + by sim. + qed. + + (* No side, non-relational goal *) + lemma L' : hoare[M.f : true ==> true]. + proof. + proc. + proc rewrite /=. + proc rewrite /=. + admit. + qed. +end BlockSimpl. + +(* -------------------------------------------------------------------- *) +(* Ranges: only the selected instructions are touched, deeply. *) +theory RangeSimpl. + module M = { + proc f(a : int, b : int) : int = { + var c, i : int; + + c <- foo a; + i <- 0; + while (i < bar b) { + if (foo i = 0) { + c <- c + foo i; + } else { + c <- c + bar i; + } + i <- i + 1; + } + return c; + } + + proc g(a : int, b : int) : int = { + var c, i : int; + + c <- foo a; + i <- 0; + while (i < b * 2) { + if (i + 1 = 0) { + c <- c + (i + 1); + } else { + c <- c + i * 2; + } + i <- i + 1; + } + return c; + } + + proc k(a : int, b : int) : int = { + var c, i : int; + + c <- foo a; + i <- 0; + while (i < bar b) { + if (i + 1 = 0) { + c <- c + (i + 1); + } else { + c <- c + bar i; + } + i <- i + 1; + } + return c; + } + }. + + lemma L : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} [3..3] /=. + by sim. + qed. + + (* A single position is the singleton range: the while body is + rewritten too *) + lemma L0 : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} 3 /=. + by sim. + qed. + + (* Range inside a nested block *) + lemma L' : equiv[M.f ~ M.k : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} ^while.:[1..1] /=. + proc rewrite {2} ^while.1?:[1..1] /=. + by sim. + qed. + + lemma L'' : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} [1..2] /=. + proc rewrite {2} [1..2] /=. + proc rewrite {1} [3..3] /=. + by sim. + qed. +end RangeSimpl. + +(* -------------------------------------------------------------------- *) +(* Match arms: the arm binders are in scope for the rewrite, even when + their names clash with the proof context. *) +theory MatchSimpl. + module M = { + proc f(o : int option) : int = { + var c : int; + + match o with + | None => c <- foo 0; + | Some x => c <- foo x; + end; + return c; + } + + proc g(o : int option) : int = { + var c : int; + + match o with + | None => c <- 0 + 1; + | Some x => c <- x + 1; + end; + return c; + } + + proc k(o : int option) : int = { + var c : int; + + match o with + | None => c <- 0 + 1; + | Some x => c <- 1 + x; + end; + return c; + } + }. + + lemma L (x : int) : equiv[M.f ~ M.g : ={arg} /\ x = 0 ==> ={res}]. + proof. + proc. + proc rewrite {1} /=. + by sim. + qed. + + lemma L' (x : int) : equiv[M.g ~ M.k : ={arg} /\ x = 0 ==> ={res}]. + proof. + proc. + proc rewrite {1} ^match#Some.:[1..1] addzC. + by sim. + qed. +end MatchSimpl. + +(* -------------------------------------------------------------------- *) +(* Lemma mode: instructions without an occurrence are skipped; the + tactic fails only when nothing is rewritten. *) +theory BlockRw. + module M = { + proc f(a : int, b : int) : int = { + var c : int; + + c <- a + b; + if (a + b = 0) { + c <- 0; + } else { + c <- c * (b + a); + } + return c; + } + + proc g(a : int, b : int) : int = { + var c : int; + + c <- b + a; + if (b + a = 0) { + c <- 0; + } else { + c <- c * (a + b); + } + return c; + } + }. + + lemma L : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} addzC. + by sim. + qed. + + lemma L' : equiv[M.f ~ M.g : ={arg} ==> ={res}]. + proof. + proc. + proc rewrite {1} [2..2] addzC. + proc rewrite {1} [1..1] addzC. + by sim. + qed. + + lemma L'' : hoare[M.f : true ==> true]. + proof. + proc. + fail proc rewrite [1..1] mulzC. + fail proc rewrite mulzA. + proc rewrite mulzC. + admit. + qed. +end BlockRw.