Skip to content

proc change: well-formed goals when introducing fresh locals #1040

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
strub merged 1 commit into from
Jun 10, 2026
+31 −24
Merged

proc change: well-formed goals when introducing fresh locals #1040

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 11 additions & 6 deletions src/ecLowPhlGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -235,13 +235,18 @@ let tc1_process_codepos1 tc (side, cpos) =
EcTyping.trans_codepos1 env cpos

(* -------------------------------------------------------------------- *)
let hl_set_stmt (side : side option) (f : form) (s : stmt) =
(* [mt] overrides the memtype of the active side (the one whose statement is
being replaced), e.g. when the new statement [s] mentions fresh locals.
The memory identifier is untouched, so the pre/post-conditions keep
referring to it. *)
let hl_set_stmt ?(mt : memtype option) (side : side option) (f : form) (s : stmt) =
let mtof (dfl : memenv) = odfl (snd dfl) mt in
match side, f.f_node with
| None , FhoareS hs -> f_hoareS (snd hs.hs_m) (hs_pr hs) s (hs_po hs)
| None , FeHoareS hs -> f_eHoareS (snd hs.ehs_m) (ehs_pr hs) s (ehs_po hs)
| None , FbdHoareS hs -> f_bdHoareS (snd hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
| Some `Left , FequivS es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)
| Some `Right, FequivS es -> f_equivS (snd es.es_ml) (snd es.es_mr) (es_pr es) es.es_sl s (es_po es)
| None , FhoareS hs -> f_hoareS (mtof hs.hs_m) (hs_pr hs) s (hs_po hs)
| None , FeHoareS hs -> f_eHoareS (mtof hs.ehs_m) (ehs_pr hs) s (ehs_po hs)
| None , FbdHoareS hs -> f_bdHoareS (mtof hs.bhs_m) (bhs_pr hs) s (bhs_po hs) hs.bhs_cmp (bhs_bd hs)
| Some `Left , FequivS es -> f_equivS (mtof es.es_ml) (snd es.es_mr) (es_pr es) s es.es_sr (es_po es)
| Some `Right, FequivS es -> f_equivS (snd es.es_ml) (mtof es.es_mr) (es_pr es) es.es_sl s (es_po es)
| _ , _ -> assert false

(* -------------------------------------------------------------------- *)
Expand Down
38 changes: 20 additions & 18 deletions src/phl/ecPhlRewrite.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -230,29 +230,27 @@ let process_rewrite_at
|> FApi.t_sub [t_pre; t_post; EcLowGoal.t_id]

(* -------------------------------------------------------------------- *)
(* [t_change_stmt side pos ?me s] replaces a code range with [s] by
(* [t_change_stmt side pos ?mt s] replaces a code range with [s] by
generating:
- a local equivalence goal showing that the original fragment and [s]
agree under the framed precondition on the variables they both read,
and produce the same values for everything observable afterwards;
- the original program-logic goal with the selected range rewritten.

If [me] is provided, it is used as the memory environment (e.g. when
fresh local variables have been bound); otherwise, the memory
environment is taken from the goal. *)
If [mt] is provided, it is used as the memtype of the selected side (e.g.
when fresh local variables have been bound); otherwise, the memtype is
taken from the goal. *)
let t_change_stmt
(side : side option)
(pos : EcMatching.Position.codegap_range)
?(me : memenv option)
?(mt : memtype option)
(s : stmt)
(tc : tcenv1)
=
let env = FApi.tc1_env tc in

let me, stmt =
let metc, stmt = EcLowPhlGoal.tc1_get_stmt side tc in
(odfl metc me, stmt)
in
let (mid, metc), stmt = EcLowPhlGoal.tc1_get_stmt side tc in
let mt = odfl metc mt in

let zpr, (_,stmt, epilog), _nmr =
EcMatching.Zipper.zipper_and_split_of_cgap_range env pos stmt in
Expand All @@ -269,8 +267,8 @@ let t_change_stmt
let frame =
let filter (f : form) =
let pvs = EcPV.form_read env EcPV.PMVS.empty f in
let pvs_me = EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs in
let pvs = EcIdent.Mid.remove (fst me) pvs in
let pvs_me = EcIdent.Mid.find_def EcPV.PV.empty mid pvs in
let pvs = EcIdent.Mid.remove mid pvs in

EcIdent.Mid.is_empty pvs
&& (EcPV.PV.indep env modi pvs_me) in
Expand All @@ -293,7 +291,7 @@ let t_change_stmt
EcLowPhlGoal.logicS_post_read env
(EcLowPhlGoal.get_logicS (FApi.tc1_goal tc))
in
EcIdent.Mid.find_def EcPV.PV.empty (fst me) pvs
EcIdent.Mid.find_def EcPV.PV.empty mid pvs
in

EcPV.PV.union obs goal
Expand All @@ -314,7 +312,7 @@ let t_change_stmt
let mr = EcIdent.create "&2" in

let frame = omap (fun frame ->
let subst = EcSubst.add_memory EcSubst.empty (fst me) ml in
let subst = EcSubst.add_memory EcSubst.empty mid ml in
EcSubst.subst_form subst frame) frame in

let mk_pv_eq ((pv, ty) : prog_var * ty) =
Expand All @@ -329,10 +327,13 @@ let t_change_stmt
let po_eq = List.map mk_pv_eq wr_pvs @ List.map mk_glob_eq wr_globs in

(* First subgoal: prove that the replacement fragment preserves the
observable behavior required by the outer proof. *)
observable behavior required by the outer proof. The left program is the
original fragment, which only mentions the pre-existing locals
([metc]); the right program is the replacement, which may use the
freshly bound locals ([mt]). *)
let goal1 =
f_equivS
(snd me) (snd me)
metc mt
{ ml; mr; inv = ofold f_and (f_ands pr_eq) frame; }
(EcAst.stmt stmt) s
{ ml; mr; inv = f_ands po_eq; }
Expand All @@ -341,10 +342,11 @@ let t_change_stmt
let stmt = EcMatching.Zipper.zip { zpr with z_tail = s.s_node @ epilog } in

(* Second subgoal: continue with the original goal after rewriting the
selected statement range. *)
selected statement range. The rewritten side also takes [mt], as the new
statement may mention the fresh locals. *)
let goal2 =
EcLowPhlGoal.hl_set_stmt
side (FApi.tc1_goal tc)
~mt side (FApi.tc1_goal tc)
stmt in

FApi.xmutate1 tc `ProcChangeStmt [goal1; goal2]
Expand Down Expand Up @@ -401,4 +403,4 @@ let process_change_stmt
let hyps = EcEnv.LDecl.push_active_ss me hyps in
let s = EcProofTyping.process_stmt hyps s in

t_change_stmt side pos ~me s tc
t_change_stmt side pos ~mt:(snd me) s tc
Loading