From b72e18cf4788f0d7d9d9ffe03b396e1c30674141 Mon Sep 17 00:00:00 2001 From: Pierre-Yves Strub Date: Mon, 2 Feb 2026 09:40:22 +0100 Subject: [PATCH] [seq]: remove bck/fwd option + cleanup The bck/fwd variants of `seq` are unused and are a leftover from CertiCrypt. No other tactic provides such variants. We may want to reintroduce them in the future, but for now this code is largely dead since it is not used by any project. Internally, the `seq` tactic was called `app`. This commit updates that. --- src/ecHiTacticals.ml | 2 +- src/ecLexer.mll | 2 - src/ecParser.mly | 17 ++----- src/ecParsetree.ml | 16 +++--- src/phl/ecPhlCall.ml | 4 +- src/phl/ecPhlEqobs.ml | 2 +- src/phl/ecPhlExists.ml | 8 +-- src/phl/ecPhlHiAuto.ml | 8 +-- src/phl/ecPhlHiCond.ml | 4 +- src/phl/ecPhlLoopTx.ml | 2 +- src/phl/{ecPhlApp.ml => ecPhlSeq.ml} | 68 ++++++++++++-------------- src/phl/{ecPhlApp.mli => ecPhlSeq.mli} | 12 ++--- src/phl/ecPhlWhile.ml | 2 +- 13 files changed, 64 insertions(+), 83 deletions(-) rename src/phl/{ecPhlApp.ml => ecPhlSeq.ml} (85%) rename src/phl/{ecPhlApp.mli => ecPhlSeq.mli} (50%) diff --git a/src/ecHiTacticals.ml b/src/ecHiTacticals.ml index 45af10852..88ce90195 100644 --- a/src/ecHiTacticals.ml +++ b/src/ecHiTacticals.ml @@ -173,7 +173,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) = | Pfun (`Upto info) -> EcPhlFun.process_fun_upto info | Pfun `Code -> EcPhlFun.process_fun_to_code | Pskip -> EcPhlSkip.t_skip - | Papp info -> EcPhlApp.process_app info + | Pseq info -> EcPhlSeq.process_seq info | Pwp wp -> EcPhlWp.process_wp wp | Psp sp -> EcPhlSp.process_sp sp | Prcond (side, b, i) -> EcPhlRCond.process_rcond side b i diff --git a/src/ecLexer.mll b/src/ecLexer.mll index e5a5ced94..b05cfe095 100644 --- a/src/ecLexer.mll +++ b/src/ecLexer.mll @@ -261,8 +261,6 @@ ("+" , (PLUS , false)); ("-" , (MINUS , false)); ("*" , (STAR , false)); - ("<<" , (BACKS , false)); - (">>" , (FWDS , false)); ("<:" , (LTCOLON , false)); ("==>" , (LONGARROW , false)); ("=" , (EQ , false)); diff --git a/src/ecParser.mly b/src/ecParser.mly index b1146388e..06f464f93 100644 --- a/src/ecParser.mly +++ b/src/ecParser.mly @@ -391,7 +391,6 @@ %token AUTO %token AXIOM %token AXIOMATIZED -%token BACKS %token BACKSLASH %token BETA %token BY @@ -457,7 +456,6 @@ %token FROM %token FUN %token FUSION -%token FWDS %token GEN %token GLOB %token GLOBAL @@ -2497,11 +2495,6 @@ call_info: | bad=form COMMA p=form { CI_upto (bad,p,None) } | bad=form COMMA p=form COMMA q=form { CI_upto (bad,p,Some q) } -tac_dir: -| BACKS { Backs } -| FWDS { Fwds } -| empty { Backs } - icodepos_r: | IF { (`If :> pcp_match) } | WHILE { (`While :> pcp_match) } @@ -2672,13 +2665,13 @@ dbhint: app_bd_info: | empty - { PAppNone } + { PSeqNone } | f=sform - { PAppSingle f } + { PSeqSingle f } | f=prod_form g=prod_form s=sform? - { PAppMult (s, fst f, snd f, fst g, snd g) } + { PSeqMult (s, fst f, snd f, fst g, snd g) } revert: | cl=ioption(brace(loc(ipcore_name)+)) gp=genpattern* @@ -2915,8 +2908,8 @@ interleave_info: | PROC STAR { Pfun `Code } -| SEQ s=side? d=tac_dir pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info - { Papp (s, d, pos, p, f) } +| SEQ s=side? pos=s_codepos1 COLON p=form_or_double_form f=app_bd_info + { Pseq (s, pos, p, f) } | WP n=s_codepos1? { Pwp n } diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml index 169e22ba8..6b4f1e2b9 100644 --- a/src/ecParsetree.ml +++ b/src/ecParsetree.ml @@ -543,10 +543,10 @@ type call_info = | CI_inv of pformula | CI_upto of (pformula * pformula * pformula option) -type p_app_xt_info = - | PAppNone - | PAppSingle of pformula - | PAppMult of (pformula option) tuple5 +type p_seq_xt_info = + | PSeqNone + | PSeqSingle of pformula + | PSeqMult of (pformula option) tuple5 type ('a, 'b, 'c) rnd_tac_info = | PNoRndParams @@ -559,8 +559,6 @@ type rnd_tac_info_f = type psemrndpos = (bool * pcodepos1) doption -type tac_dir = Backs | Fwds - type pfel_spec_preds = (pgamepath * pformula) list (* -------------------------------------------------------------------- *) @@ -618,8 +616,8 @@ type fun_info = [ ] (* -------------------------------------------------------------------- *) -type app_info = - oside * tac_dir * pcodepos1 doption * pformula doption * p_app_xt_info +type seq_info = + oside * pcodepos1 doption * pformula doption * p_seq_xt_info (* -------------------------------------------------------------------- *) type pcond_info = [ @@ -726,7 +724,7 @@ type phltactic = | Pskip | Prepl_stmt of trans_info | Pfun of fun_info - | Papp of app_info + | Pseq of seq_info | Pwp of pdocodepos1 | Psp of pdocodepos1 | Pwhile of (oside * while_info) diff --git a/src/phl/ecPhlCall.ml b/src/phl/ecPhlCall.ml index 8231b9f27..294512570 100644 --- a/src/phl/ecPhlCall.ml +++ b/src/phl/ecPhlCall.ml @@ -145,14 +145,14 @@ let t_ehoare_call_core fpre fpost tc = let t_ehoare_call fpre fpost tc = let _, _, _, s, _, wppre, _ = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in + EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) wppre tc in let tcenv = FApi.t_swap_goals 0 1 tcenv in FApi.t_sub [t_ehoare_call_core fpre fpost; t_id] tcenv let t_ehoare_call_concave f fpre fpost tc = let _, _, _, s, _, wppre, wppost = ehoare_call_pre_post fpre fpost tc in let tcenv = - EcPhlApp.t_ehoare_app (EcMatching.Zipper.cpos (List.length s.s_node)) + EcPhlSeq.t_ehoare_seq (EcMatching.Zipper.cpos (List.length s.s_node)) (map_ss_inv2 (fun wppre f -> f_app_simpl f [wppre] txreal) wppre f) tc in let tcenv = FApi.t_swap_goals 0 1 tcenv in let t_call = diff --git a/src/phl/ecPhlEqobs.ml b/src/phl/ecPhlEqobs.ml index 8466ac935..461f570e2 100644 --- a/src/phl/ecPhlEqobs.ml +++ b/src/phl/ecPhlEqobs.ml @@ -476,7 +476,7 @@ let process_eqobs_inS info tc = let _, eqi = try s_eqobs_in_full (stmt sl2) (stmt sr2) sim Mpv2.empty_local eqo with EqObsInError -> tc_error !!tc "cannot apply sim" in - (EcPhlApp.t_equiv_app (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [ + (EcPhlSeq.t_equiv_seq (p1, p2) (Mpv2.to_form_ts_inv eqi inv) @+ [ t_id; fun tc -> FApi.t_last diff --git a/src/phl/ecPhlExists.ml b/src/phl/ecPhlExists.ml index 70776aceb..dcc36981d 100644 --- a/src/phl/ecPhlExists.ml +++ b/src/phl/ecPhlExists.ml @@ -153,16 +153,16 @@ let process_ecall oside (l, tvi, fs) tc = let t_local_seq p1 tc = match kind, oside, p1 with | `Hoare n, _, Inv_ss p1 -> - EcPhlApp.t_hoare_app + EcPhlSeq.t_hoare_seq (Zpr.cpos (n-1)) p1 tc | `Equiv (n1, n2), None, Inv_ts p1 -> - EcPhlApp.t_equiv_app + EcPhlSeq.t_equiv_seq (Zpr.cpos (n1-1), Zpr.cpos (n2-1)) p1 tc | `Equiv (n1, n2), Some `Left, Inv_ts p1 -> - EcPhlApp.t_equiv_app + EcPhlSeq.t_equiv_seq (Zpr.cpos (n1-1), Zpr.cpos n2) p1 tc | `Equiv(n1, n2), Some `Right, Inv_ts p1 -> - EcPhlApp.t_equiv_app + EcPhlSeq.t_equiv_seq (Zpr.cpos n1, Zpr.cpos (n2-1)) p1 tc | _ -> tc_error !!tc "mismatched sidedness or kind of conclusion" in diff --git a/src/phl/ecPhlHiAuto.ml b/src/phl/ecPhlHiAuto.ml index c74f27ce3..c5c23d645 100644 --- a/src/phl/ecPhlHiAuto.ml +++ b/src/phl/ecPhlHiAuto.ml @@ -68,7 +68,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = | LL_JUMP -> let m = EcIdent.create "&hr" in - ( EcPhlApp.t_bdhoare_app + ( EcPhlSeq.t_bdhoare_seq (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) @@ -86,7 +86,7 @@ and apply_ll_strategy1 (lls : ll_strategy) tc = @+ [apply_ll_strategy lls1; apply_ll_strategy lls2] in - ( EcPhlApp.t_bdhoare_app + ( EcPhlSeq.t_bdhoare_seq (Zpr.cpos (-1)) ({m;inv=f_true}, {m;inv=f_true}, {m;inv=f_r1}, {m;inv=f_r1}, {m;inv=f_r0}, {m;inv=f_r1}) @~ FApi.t_onalli (function @@ -142,8 +142,8 @@ let t_lossless tc = | FequivS hs -> let ml, mr = fst hs.es_ml, fst hs.es_mr in - ((EcPhlApp.t_equiv_app_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ - [ (EcPhlApp.t_equiv_app_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ + ((EcPhlSeq.t_equiv_seq_onesided `Left (EcMatching.Zipper.cpos 0) {m=ml;inv=f_true} {m=ml;inv=f_true}) @+ + [ (EcPhlSeq.t_equiv_seq_onesided `Right (EcMatching.Zipper.cpos 0) {m=mr;inv=f_true} {m=mr;inv=f_true}) @+ [ EcPhlSkip.t_skip @! t_trivial ; t_single ]; diff --git a/src/phl/ecPhlHiCond.ml b/src/phl/ecPhlHiCond.ml index 89225fb4d..5c0e6921d 100644 --- a/src/phl/ecPhlHiCond.ml +++ b/src/phl/ecPhlHiCond.ml @@ -26,7 +26,7 @@ let process_cond (info : EcParsetree.pcond_info) tc = let i2 = Option.map (fun i2 -> EcLowPhlGoal.tc1_process_codepos1 tc (side, i2)) i2 in let n1 = default_if i1 es.es_sl in let n2 = default_if i2 es.es_sr in - FApi.t_seqsub (EcPhlApp.t_equiv_app (n1, n2) f) + FApi.t_seqsub (EcPhlSeq.t_equiv_seq (n1, n2) f) [ t_id; t_equiv_cond side ] tc | `SeqOne (s, i, f1, f2) -> @@ -36,7 +36,7 @@ let process_cond (info : EcParsetree.pcond_info) tc = let _, f1 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f1 in let _, f2 = EcProofTyping.tc1_process_Xhl_formula ~side:s tc f2 in FApi.t_seqsub - (EcPhlApp.t_equiv_app_onesided s n f1 f2) + (EcPhlSeq.t_equiv_seq_onesided s n f1 f2) [ t_id; t_bdhoare_cond] tc (* -------------------------------------------------------------------- *) diff --git a/src/phl/ecPhlLoopTx.ml b/src/phl/ecPhlLoopTx.ml index 434dece2c..0844ab2f2 100644 --- a/src/phl/ecPhlLoopTx.ml +++ b/src/phl/ecPhlLoopTx.ml @@ -320,7 +320,7 @@ let process_unroll_for side cpos tc = let (h', pos', z') = oget hds.(i-1) in FApi.t_seqs [ EcPhlWp.t_wp (Some (Single (Zpr.cpos (pos-2)))); - EcPhlApp.t_hoare_app (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ + EcPhlSeq.t_hoare_seq (Zpr.cpos (pos' - 1)) (map_ss_inv2 f_eq x {m=goal_m;inv=f_int z'}) @+ [t_apply_hd h'; t_conseq_nm] ] tc in diff --git a/src/phl/ecPhlApp.ml b/src/phl/ecPhlSeq.ml similarity index 85% rename from src/phl/ecPhlApp.ml rename to src/phl/ecPhlSeq.ml index 2d2ea618b..e829480d0 100644 --- a/src/phl/ecPhlApp.ml +++ b/src/phl/ecPhlSeq.ml @@ -14,7 +14,7 @@ open EcLowPhlGoal module TTC = EcProofTyping (* -------------------------------------------------------------------- *) -let t_hoare_app_r i phi tc = +let t_hoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_hoareS tc in let phi = ss_inv_rebind phi (fst hs.hs_m) in @@ -23,10 +23,10 @@ let t_hoare_app_r i phi tc = let b = f_hoareS (snd hs.hs_m) phi (stmt s2) (hs_po hs) in FApi.xmutate1 tc `HlApp [a; b] -let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r +let t_hoare_seq = FApi.t_low2 "hoare-seq" t_hoare_seq_r (* -------------------------------------------------------------------- *) -let t_ehoare_app_r i phi tc = +let t_ehoare_seq_r i phi tc = let env = FApi.tc1_env tc in let hs = tc1_as_ehoareS tc in let s1, s2 = s_split env i hs.ehs_s in @@ -35,10 +35,10 @@ let t_ehoare_app_r i phi tc = let b = f_eHoareS (snd hs.ehs_m) phi (stmt s2) (ehs_po hs) in FApi.xmutate1 tc `HlApp [a; b] -let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r +let t_ehoare_seq = FApi.t_low2 "hoare-seq" t_ehoare_seq_r (* -------------------------------------------------------------------- *) -let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc = +let t_bdhoare_seq_r_low i (phi, pR, f1, f2, g1, g2) tc = let env = FApi.tc1_env tc in let bhs = tc1_as_bdhoareS tc in let m = fst bhs.bhs_m in @@ -93,7 +93,7 @@ let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc = FApi.xmutate1 tc `HlApp conds (* -------------------------------------------------------------------- *) -let t_bdhoare_app_r i info tc = +let t_bdhoare_seq_r i info tc = let tactic tc = let hs = tc1_as_hoareS tc in let tt1 = EcPhlConseq.t_hoareS_conseq_nm (hs_pr hs) {m=(fst hs.hs_m);inv=f_true} in @@ -103,12 +103,12 @@ let t_bdhoare_app_r i info tc = FApi.t_last (FApi.t_try (t_intros_s_seq (`Symbol ["_"; "_"]) tactic)) - (t_bdhoare_app_r_low i info tc) + (t_bdhoare_seq_r_low i info tc) -let t_bdhoare_app = FApi.t_low2 "bdhoare-app" t_bdhoare_app_r +let t_bdhoare_seq = FApi.t_low2 "bdhoare-seq" t_bdhoare_seq_r (* -------------------------------------------------------------------- *) -let t_equiv_app (i, j) phi tc = +let t_equiv_seq (i, j) phi tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in let sl1,sl2 = s_split env i es.es_sl in @@ -119,7 +119,7 @@ let t_equiv_app (i, j) phi tc = FApi.xmutate1 tc `HlApp [a; b] -let t_equiv_app_onesided side i pre post tc = +let t_equiv_seq_onesided side i pre post tc = let env = FApi.tc1_env tc in let es = tc1_as_equivS tc in let (ml, mr) = fst es.es_ml, fst es.es_mr in @@ -143,7 +143,7 @@ let t_equiv_app_onesided side i pre post tc = let modi = EcPV.s_write env (EcModules.stmt s2) in let r = map_ts_inv2 f_and p' (generalize_mod_side env modi (map_ts_inv2 f_imp q' (es_po es))) in - FApi.t_seqsub (t_equiv_app ij r) + FApi.t_seqsub (t_equiv_seq ij r) [t_id; (* s1 ~ s' : pr ==> r *) FApi.t_seqsub (EcPhlConseq.t_equivS_conseq_nm p' q') [(* r => forall mod, post => post' *) t_trivial; @@ -153,31 +153,23 @@ let t_equiv_app_onesided side i pre post tc = ] tc (* -------------------------------------------------------------------- *) -let process_phl_bd_info dir bd_info tc = +let process_phl_bd_info bd_info tc = match bd_info with - | PAppNone -> + | PSeqNone -> let hs = tc1_as_bdhoareS tc in let m = fst hs.bhs_m in - let f1, f2 = - match dir with - | Backs -> bhs_bd hs, {m;inv=f_r1} - | Fwds -> {m;inv=f_r1}, bhs_bd hs - in + let f1, f2 = bhs_bd hs, {m;inv=f_r1} in (* The last argument will not be used *) ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) - | PAppSingle f -> + | PSeqSingle f -> let hs = tc1_as_bdhoareS tc in let m = fst hs.bhs_m in let f = snd (TTC.tc1_process_Xhl_form tc treal f) in - let f1, f2 = - match dir with - | Backs -> (map_ss_inv2 f_real_div (bhs_bd hs) f, f) - | Fwds -> (f, map_ss_inv2 f_real_div (bhs_bd hs) f) - in + let f1, f2 = (map_ss_inv2 f_real_div (bhs_bd hs) f, f) in ({m;inv=f_true}, f1, f2, {m;inv=f_r0}, {m;inv=f_r1}) - | PAppMult (phi, f1, f2, g1, g2) -> + | PSeqMult (phi, f1, f2, g1, g2) -> let hs = tc1_as_bdhoareS tc in let m = fst hs.bhs_m in let phi = @@ -212,7 +204,7 @@ let process_phl_bd_info dir bd_info tc = (phi, f1, f2, g1, g2) (* -------------------------------------------------------------------- *) -let process_app (side, dir, k, phi, bd_info) tc = +let process_seq ((side, k, phi, bd_info) : seq_info) (tc : tcenv1) = let concl = FApi.tc1_goal tc in let get_single phi = @@ -225,19 +217,19 @@ let process_app (side, dir, k, phi, bd_info) tc = tc_error !!tc "seq: no side information expected" in match k, bd_info with - | Single i, PAppNone when is_hoareS concl -> + | Single i, PSeqNone when is_hoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in - t_hoare_app i phi tc + t_hoare_seq i phi tc - | Single i, PAppNone when is_eHoareS concl -> + | Single i, PSeqNone when is_eHoareS concl -> check_side side; let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in - t_ehoare_app i phi tc + t_ehoare_seq i phi tc - | Single i, PAppNone when is_equivS concl -> + | Single i, PSeqNone when is_equivS concl -> let pre, post = match phi with | Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected" @@ -250,24 +242,24 @@ let process_app (side, dir, k, phi, bd_info) tc = | None -> tc_error !!tc "seq onsided: side information expected" | Some side -> side in let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some side, i) in - t_equiv_app_onesided side i pre post tc + t_equiv_seq_onesided side i pre post tc | Single i, _ when is_bdHoareS concl -> check_side side; let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in - let (ra, f1, f2, f3, f4) = process_phl_bd_info dir bd_info tc in + let (ra, f1, f2, f3, f4) = process_phl_bd_info bd_info tc in let i = EcLowPhlGoal.tc1_process_codepos1 tc (side, i) in - t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc + t_bdhoare_seq i (ra, pia, f1, f2, f3, f4) tc - | Double (i, j), PAppNone when is_equivS concl -> + | Double (i, j), PSeqNone when is_equivS concl -> check_side side; let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in let i = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, i) in let j = EcLowPhlGoal.tc1_process_codepos1 tc (Some `Left, j) in - t_equiv_app (i, j) phi tc + t_equiv_seq (i, j) phi tc - | Single _, PAppNone - | Double _, PAppNone -> + | Single _, PSeqNone + | Double _, PSeqNone -> tc_error !!tc "invalid `position' parameter" | _, _ -> diff --git a/src/phl/ecPhlApp.mli b/src/phl/ecPhlSeq.mli similarity index 50% rename from src/phl/ecPhlApp.mli rename to src/phl/ecPhlSeq.mli index 41d089476..b5b905ad5 100644 --- a/src/phl/ecPhlApp.mli +++ b/src/phl/ecPhlSeq.mli @@ -6,11 +6,11 @@ open EcMatching.Position open EcAst (* -------------------------------------------------------------------- *) -val t_hoare_app : codepos1 -> ss_inv -> backward -val t_ehoare_app : codepos1 -> ss_inv -> backward -val t_bdhoare_app : codepos1 -> ss_inv tuple6 -> backward -val t_equiv_app : codepos1 pair -> ts_inv -> backward -val t_equiv_app_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward +val t_hoare_seq : codepos1 -> ss_inv -> backward +val t_ehoare_seq : codepos1 -> ss_inv -> backward +val t_bdhoare_seq : codepos1 -> ss_inv tuple6 -> backward +val t_equiv_seq : codepos1 pair -> ts_inv -> backward +val t_equiv_seq_onesided : side -> codepos1 -> ss_inv -> ss_inv -> backward (* -------------------------------------------------------------------- *) -val process_app : app_info -> backward +val process_seq : seq_info -> backward diff --git a/src/phl/ecPhlWhile.ml b/src/phl/ecPhlWhile.ml index c54b43ea4..1d1136c94 100644 --- a/src/phl/ecPhlWhile.ml +++ b/src/phl/ecPhlWhile.ml @@ -108,7 +108,7 @@ let t_ehoare_while inv tc = let m = EcMemory.memory hs.ehs_m in let e = ss_inv_of_expr m e in let tc = - FApi.t_rotate `Left 1 (EcPhlApp.t_ehoare_app (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in + FApi.t_rotate `Left 1 (EcPhlSeq.t_ehoare_seq (0, `ByPos (List.length hs.ehs_s.s_node - 1)) inv tc) in FApi.t_sub [(EcPhlConseq.t_ehoareS_conseq inv (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not e) inv)) @+ [t_trivial;