Refactor ecPhlConseq.ml: restructure, deduplicate, document, and annotate by strub · Pull Request #965 · EasyCrypt/easycrypt

strub · 2026-04-03T18:20:22Z

Split the ~500-line monolithic t_hi_conseq dispatcher into 8
per-goal-type functions (hoareS/F, bdHoareS/F, ehoareS/F, equivS/F)
with a thin top-level dispatcher
Extract shared helpers (t_hi_trivial, t_hi_apply_r, etc.) to module
level
Unify three identical gen_conseq_nm variants into a single polymorphic
one
Factor shared proof-term processing pipeline into process_conseq_core;
rename process_conseq_1/2 to process_conseq_hs/ss for clarity
Extract cond_F_notmod_core / cond_S_notmod_core shared helpers,
reducing cond_{hoare,bdHoare}{F,S}_notmod to 3-line wrappers
Remove unnecessary ~recurse indirection from equivS/equivF dispatchers
(make them directly recursive instead)
Introduce hi_arg type alias and add type annotations to all top-level
functions
Add inference-rule comments to every goal-closing tactic and document
the processing pipeline, naming conventions, and section structure

…tate - Split the ~500-line monolithic t_hi_conseq dispatcher into 8 per-goal-type functions (hoareS/F, bdHoareS/F, ehoareS/F, equivS/F) with a thin top-level dispatcher - Extract shared helpers (t_hi_trivial, t_hi_apply_r, etc.) to module level - Unify three identical gen_conseq_nm variants into a single polymorphic one - Factor shared proof-term processing pipeline into process_conseq_core; rename process_conseq_1/2 to process_conseq_hs/ss for clarity - Extract cond_F_notmod_core / cond_S_notmod_core shared helpers, reducing cond_{hoare,bdHoare}{F,S}_notmod to 3-line wrappers - Remove unnecessary ~recurse indirection from equivS/equivF dispatchers (make them directly recursive instead) - Introduce hi_arg type alias and add type annotations to all top-level functions - Add inference-rule comments to every goal-closing tactic and document the processing pipeline, naming conventions, and section structure

Gustavo2622 · 2026-04-07T16:52:19Z

src/phl/ecPhlConseq.ml

+ *   ——————————————————————————————————————————————————————————
+ *                    ehoare[f] P ==> Q
+ *
+ * Note: for ehoare, the direction is reversed (xreal_le) compared


Somewhat confusing comment, I would suggest "xreal_le (<=) is the ehoare analogue of implication (=>)"

Gustavo2622 · 2026-04-07T16:54:16Z

src/phl/ecPhlConseq.ml

-let t_bdHoareF_conseq pre post tc =
+(* bdHoareF consequence rule:
+ *
+ *   ∀m, P m ⇒ P' m    ∀m, Q' m ⇒/⇔ Q m    phoare[f] P' ==> Q' cmp bd


Minor: missing one of the directions for postcondition implication

Gustavo2622 · 2026-04-07T17:03:51Z

src/phl/ecPhlConseq.ml

+(* t_*_conseq_nm: combines notmod with consequence                       *)
+(* -------------------------------------------------------------------- *)
+
+let mk_bind_pvar (m : memory) (id,_) (x, ty) =


Maybe move utility functions to other file?

Gustavo2622 · 2026-04-07T17:06:52Z

src/phl/ecPhlConseq.ml

+let mk_bind_globs (env : env) (m : memory) (bd1,bd2) =
+  List.map2 (mk_bind_glob env m) bd1 bd2
+
+let cond_equivF_notmod ?(mk_other=false) (tc : tcenv1) (cond : ts_inv) =


Add small description of notmod condition

Gustavo2622 · 2026-04-07T17:11:14Z

src/phl/ecPhlConseq.ml

-let t_equivF_notmod post tc =
+(* equivF notmod rule:
+ *
+ *   ∀ml mr, P ml mr ⇒ ∀res_L res_R modified_vars, Q' ml mr ⇒ Q ml mr


Slightly unclear term separation, quantifier bindings and what modified_vars is here

Gustavo2622 · 2026-04-07T17:35:46Z

src/phl/ecPhlConseq.ml

-  let f = hf.hf_f in
-  let mpr,mpo = Fun.hoareF_memenv hf.hf_m f env in
+(* Shared core for F-level notmod: substitutes the result variable,     *)
+(* generalizes over modified variables, quantifies over the result,     *)


Maybe be a bit clearer on what the result of this function is? (return type + what holds over the return objects)

Gustavo2622 · 2026-04-07T17:40:28Z

src/phl/ecPhlConseq.ml

+(* hoareF notmod rule:
+ *
+ *   ∀m, P m ⇒ ∀res modified_vars, Q' m ⇒ Q m [∧ Qe]
+ *   hoare[f] P ==> Q'[/Qe']


Unclear notation

Gustavo2622 · 2026-04-07T17:41:11Z

src/phl/ecPhlConseq.ml

-let t_bdHoareF_notmod post tc =
+(* bdHoareF notmod rule:
+ *
+ *   ∀m, P m ⇒ ∀res modified_vars, Q' m ⇒/⇔ Q m


Same as above, slightly unclear

Gustavo2622 · 2026-04-07T17:45:03Z

src/phl/ecPhlConseq.ml


 (* -------------------------------------------------------------------- *)
-let t_ehoareF_conseq_nm pre post tc =
+let t_ehoareF_conseq_nm (pre : ss_inv) (post : ss_inv) (tc : tcenv1) =


Suggestion: maybe move above concavity to group not mod rules? Results in a bigger diff but better organization

Gustavo2622 · 2026-04-07T17:47:49Z

src/phl/ecPhlConseq.ml

+ *   hoare[c] P ==> post     phoare[c] P ==> post' ∧ post cmp bd
+ *   —————————————————————————————————————————————————————————————
+ *              phoare[c] P ==> post' cmp bd
+ *


Difference between add=false and add=true unclear

Gustavo2622 · 2026-04-07T17:55:14Z

src/phl/ecPhlConseq.ml


-let t_ehoareF_conseq_equiv f2 p q p2 q2 tc =
+(* ehoareF via equivalence: similar to hoareF but with xreal ordering.
+ *   cond1: ∀m1, ∃m2, P1 m1 = ⊥ ∨ (P m1 m2 ∧ P2 m2 ≤ P1 m1)


extraneous \bot ?

Gustavo2622 · 2026-04-07T17:58:55Z

src/phl/ecPhlConseq.ml

-  let t_apply_r (pt, _f) tc =
-    match pt with
-    | Some pt -> EcLowGoal.Apply.t_apply_bwd_hi ~dpe:true pt tc
+let t_hi_trivial =


Move helper + print functions? From here to L1333

Gustavo2622 · 2026-04-07T18:01:43Z

src/phl/ecPhlConseq.ml

+(* ehoareF via equivalence: similar to hoareF but with xreal ordering.
+ *   cond1: ∀m1, ∃m2, P1 m1 = ⊥ ∨ (P m1 m2 ∧ P2 m2 ≤ P1 m1)
+ *   cond2: ∀m1 m2, Q m1 m2 ⇒ Q1 m1 ≤ Q2 m2                        *)
+let t_ehoareF_conseq_equiv


Missing ehoareS version?

Gustavo2622 · 2026-04-07T18:02:30Z

src/phl/ecPhlConseq.ml

+(* Supported combinations (goal / f1 / f2 / f3):                         *)
+(*   bdhoareF / bdhoareF / ⊥      / ⊥ — consequence with bound change   *)
+(*   bdhoareF / bdhoareF / hoareF / ⊥ — conjunction with hoare side-cond *)
+(*   bdhoareF / equivF   / bdhoareF/ _ — transitivity via equiv          *)


Also no transitivity for S?

Gustavo2622 · 2026-04-07T18:02:57Z

src/phl/ecPhlConseq.ml

+(*                                                                       *)
+(* Supported combinations (goal / f1 / f2 / f3):                         *)
+(*   equivS / equivS   / ⊥        / ⊥        — simple consequence       *)
+(*   equivS / equivS   / hoareS   / hoareS   — conjunction (L+R+rel)    *)


rel + L + R?

Gustavo2622 · 2026-04-07T18:07:22Z

src/phl/ecPhlConseq.ml

+(*                                                                       *)
+(* Supported combinations (goal / f1 / f2 / f3):                         *)
+(*   equivF / equivF / ⊥      / ⊥      — simple consequence             *)
+(*   equivF / equivF / hoareF / hoareF — conjunction (L+R+rel)          *)


Same as above, rel + L + R?

strub requested a review from Gustavo2622 April 7, 2026 10:07

strub self-assigned this Apr 7, 2026

strub added chore Ungrateful tasks that need done but that nobody wants to do technical-debt labels Apr 7, 2026

strub force-pushed the conseq-refactor branch from 765593d to b555fdc Compare April 7, 2026 14:57

strub force-pushed the conseq-refactor branch from b555fdc to 03238b5 Compare April 7, 2026 15:02

strub changed the title ~~Refactor ecPhlConseq.ml: break up monolithic dispatcher and document~~ Refactor ecPhlConseq.ml: restructure, deduplicate, document, and annotate Apr 7, 2026

strub marked this pull request as ready for review April 7, 2026 15:04

Gustavo2622 reviewed Apr 7, 2026

View reviewed changes

Conversation

strub commented Apr 3, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

strub commented Apr 3, 2026 •

edited

Loading