Skip to content

Commit afbb8b7

Browse files
strubstrub
committed
Add forward ecall with framed preconditions
This extends ecall to support forward calls on Hoare goals via ->>, while keeping backward behavior for existing uses. It refactors call postcondition generation into reusable helpers, adds proof-term/program-variable substitution utilities needed to instantiate contracts cleanly, and checks that the supplied contract matches the targeted procedure(s). For forward Hoare calls, the tactic now automatically frames precondition conjuncts that are independent of the call’s writes. A regression test is added in tests/forward-call.ec.
1 parent 0d1602f commit afbb8b7

18 files changed

Lines changed: 1129 additions & 228 deletions

‎src/ecAst.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -480,6 +480,7 @@ val pv_hash : prog_var hash
480480
val pv_fv : prog_var fv
481481

482482
val pv_kind : prog_var -> pvar_kind
483+
483484
(* -------------------------------------------------------------------- *)
484485
val idty_equal : (EcIdent.t * ty) equality
485486
val idty_hash : (EcIdent.t * ty) hash

‎src/ecEnv.ml‎

Lines changed: 18 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3569,30 +3569,40 @@ module LDecl = struct
35693569
let fresh_id hyps s = fresh_id (tohyps hyps) s
35703570
let fresh_ids hyps s = snd (fresh_ids (tohyps hyps) s)
35713571
3572+
(* ------------------------------------------------------------------ *)
3573+
let mapenv (f : env -> env) (lenv : hyps) =
3574+
{ lenv with le_env = f lenv.le_env }
3575+
35723576
(* ------------------------------------------------------------------ *)
35733577
let push_active_ss m lenv =
3574-
{ lenv with le_env = Memory.push_active_ss m lenv.le_env }
3578+
mapenv (Memory.push_active_ss m) lenv
35753579
35763580
let push_active_ts ml mr lenv =
3577-
{ lenv with le_env = Memory.push_active_ts ml mr lenv.le_env }
3581+
mapenv (Memory.push_active_ts ml mr) lenv
35783582
35793583
let push_all l lenv =
3580-
{ lenv with le_env = Memory.push_all l lenv.le_env }
3584+
mapenv (Memory.push_all l) lenv
3585+
3586+
let push_active_all l lenv =
3587+
let lenv = mapenv (Memory.push_all l) lenv in
3588+
3589+
match l with
3590+
| [(m, _)] -> mapenv (Memory.set_active_ss m) lenv
3591+
| _ -> lenv
35813592
35823593
let hoareF mem xp lenv =
35833594
let env1, env2 = Fun.hoareF mem xp lenv.le_env in
3584-
{ lenv with le_env = env1}, {lenv with le_env = env2 }
3595+
{ lenv with le_env = env1 }, { lenv with le_env = env2 }
35853596
35863597
let equivF ml mr xp1 xp2 lenv =
35873598
let env1, env2 = Fun.equivF ml mr xp1 xp2 lenv.le_env in
3588-
{ lenv with le_env = env1}, {lenv with le_env = env2 }
3599+
{ lenv with le_env = env1 }, { lenv with le_env = env2 }
35893600
35903601
let inv_memenv ml mr lenv =
3591-
{ lenv with le_env = Fun.inv_memenv ml mr lenv.le_env }
3602+
mapenv (Fun.inv_memenv ml mr) lenv
35923603
35933604
let inv_memenv1 m lenv =
3594-
{ lenv with le_env = Fun.inv_memenv1 m lenv.le_env }
3605+
mapenv (Fun.inv_memenv1 m) lenv
35953606
end
35963607
3597-
35983608
let pp_debug_form = ref (fun _env _f -> assert false)

‎src/ecEnv.mli‎

Lines changed: 4 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -515,9 +515,10 @@ module LDecl : sig
515515

516516
val clear : ?leniant:bool -> EcIdent.Sid.t -> hyps -> hyps
517517

518-
val push_all : memenv list -> hyps -> hyps
519-
val push_active_ss : memenv -> hyps -> hyps
520-
val push_active_ts : memenv -> memenv -> hyps -> hyps
518+
val push_all : memenv list -> hyps -> hyps
519+
val push_active_all : memenv list -> hyps -> hyps
520+
val push_active_ss : memenv -> hyps -> hyps
521+
val push_active_ts : memenv -> memenv -> hyps -> hyps
521522

522523
val hoareF : memory -> xpath -> hyps -> hyps * hyps
523524
val equivF : memory -> memory -> xpath -> xpath -> hyps -> hyps * hyps

‎src/ecHiTacticals.ml‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
206206
| Pconcave info -> EcPhlConseq.process_concave info
207207
| Phrex_elim -> EcPhlExists.t_hr_exists_elim
208208
| Phrex_intro (fs, b) -> EcPhlExists.process_exists_intro ~elim:b fs
209-
| Phecall (oside, x) -> EcPhlExists.process_ecall oside x
209+
| Phecall (d, s, data) -> EcPhlExists.process_ecall d s data
210210
| Pexfalso -> EcPhlAuto.t_exfalso
211211
| Pbydeno (mode, info) -> EcPhlDeno.process_deno mode info
212212
| Pbyupto -> EcPhlUpto.process_uptobad

‎src/ecMatching.ml‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -705,6 +705,10 @@ module EV = struct
705705
| Some (`Set _) -> true
706706
| _ -> false
707707

708+
let map (f : 'a -> 'a) (m : 'a evmap) =
709+
{ ev_map = Mid.map (omap f) m.ev_map
710+
; ev_unset = m.ev_unset }
711+
708712
let doget (x : ident) (m : 'a evmap) =
709713
match get x m with
710714
| Some (`Set a) -> a

‎src/ecMatching.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -318,6 +318,7 @@ module EV : sig
318318
val isset : ident -> 'a evmap -> bool
319319
val set : ident -> 'a -> 'a evmap -> 'a evmap
320320
val get : ident -> 'a evmap -> [`Unset | `Set of 'a] option
321+
val map : ('a -> 'a) -> 'a evmap -> 'a evmap
321322
val doget : ident -> 'a evmap -> 'a
322323
val fold : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b
323324
val filled : 'a evmap -> bool

‎src/ecPV.ml‎

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -156,6 +156,9 @@ module PVM = struct
156156
try Mid.change (fun o -> Some (Mpv.add env pv f (odfl Mpv.empty o))) m s
157157
with AliasClash (env,c) -> uerror env c
158158

159+
let of_list env pvs =
160+
List.fold_left (fun s ((pv, m), f) -> add env pv m f s) empty pvs
161+
159162
let find env pv m s =
160163
try Mpv.find env pv (Mid.find m s)
161164
with AliasClash (env,c) -> uerror env c
@@ -581,6 +584,11 @@ let rec e_read_r env r e =
581584
| Evar pv -> PV.add env pv e.e_ty r
582585
| _ -> e_fold (e_read_r env) r e
583586

587+
let rec form_read_r env r f =
588+
match f.f_node with
589+
| Fpvar (pv, _) -> PV.add env pv f.f_ty r
590+
| _ -> f_fold (form_read_r env) r f
591+
584592
let rec is_read_r env w s =
585593
List.fold_left (i_read_r env) w s
586594

@@ -625,11 +633,12 @@ let is_write ?(except=Sx.empty) env is = is_write_r ~except env PV.empty is
625633
let s_write ?(except=Sx.empty) env s = s_write_r ~except env PV.empty s
626634
let f_write ?(except=Sx.empty) env f = f_write_r ~except env PV.empty f
627635

628-
let e_read env e = e_read_r env PV.empty e
629-
let i_read env i = i_read_r env PV.empty i
630-
let is_read env is = is_read_r env PV.empty is
631-
let s_read env s = s_read_r env PV.empty s
632-
let f_read env f = f_read_r env PV.empty f
636+
let e_read env e = e_read_r env PV.empty e
637+
let form_read env e = form_read_r env PV.empty e
638+
let i_read env i = i_read_r env PV.empty i
639+
let is_read env is = is_read_r env PV.empty is
640+
let s_read env s = s_read_r env PV.empty s
641+
let f_read env f = f_read_r env PV.empty f
633642

634643
(* -------------------------------------------------------------------- *)
635644
let zpr_pv (kind : [ `Read | `Write ]) (span : [ `Before | `After ]) (env : env) =

‎src/ecPV.mli‎

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -71,6 +71,8 @@ module PVM : sig
7171

7272
val add : env -> prog_var -> EcIdent.t -> form -> subst -> subst
7373

74+
val of_list : env -> ((prog_var * EcIdent.t) * form) list -> subst
75+
7476
val add_glob : env -> mpath -> EcIdent.t -> form -> subst -> subst
7577

7678
val of_mpv : (form,form) Mpv.t -> EcIdent.t -> subst
@@ -127,11 +129,12 @@ val is_write_r : ?except:Sx.t -> instr list pvaccess
127129
val s_write_r : ?except:Sx.t -> stmt pvaccess
128130
val f_write_r : ?except:Sx.t -> xpath pvaccess
129131

130-
val e_read_r : expr pvaccess
131-
val i_read_r : instr pvaccess
132-
val is_read_r : instr list pvaccess
133-
val s_read_r : stmt pvaccess
134-
val f_read_r : xpath pvaccess
132+
val e_read_r : expr pvaccess
133+
val form_read_r : form pvaccess
134+
val i_read_r : instr pvaccess
135+
val is_read_r : instr list pvaccess
136+
val s_read_r : stmt pvaccess
137+
val f_read_r : xpath pvaccess
135138

136139
(* -------------------------------------------------------------------- *)
137140
type 'a pvaccess0 = env -> 'a -> PV.t
@@ -142,11 +145,12 @@ val is_write : ?except:Sx.t -> instr list pvaccess0
142145
val s_write : ?except:Sx.t -> stmt pvaccess0
143146
val f_write : ?except:Sx.t -> xpath pvaccess0
144147

145-
val e_read : expr pvaccess0
146-
val i_read : instr pvaccess0
147-
val is_read : instr list pvaccess0
148-
val s_read : stmt pvaccess0
149-
val f_read : xpath pvaccess0
148+
val e_read : expr pvaccess0
149+
val form_read : form pvaccess0
150+
val i_read : instr pvaccess0
151+
val is_read : instr list pvaccess0
152+
val s_read : stmt pvaccess0
153+
val f_read : xpath pvaccess0
150154

151155
(* -------------------------------------------------------------------- *)
152156
val zpr_pv :

‎src/ecParser.mly‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2999,6 +2999,10 @@ interleave_info:
29992999
| TILD f=loc(fident) { OKproc(f, true) }
30003000
| f=loc(fident) { OKproc(f, false) }
30013001

3002+
direction:
3003+
| RRARROW { (`Forward :> pdirection) }
3004+
| LLARROW { (`Backward :> pdirection) }
3005+
30023006
%public phltactic:
30033007
| PROC
30043008
{ Pfun `Def }
@@ -3184,8 +3188,8 @@ interleave_info:
31843188

31853189
{ Phrex_intro (l, b) }
31863190

3187-
| ECALL s=side? x=paren(p=qident tvi=tvars_app? fs=sform* { (p, tvi, fs) })
3188-
{ Phecall (s, x) }
3191+
| ECALL d=direction? s=side? x=paren(p=qident tvi=tvars_app? fs=loc(gpterm_arg)* { (p, tvi, fs) })
3192+
{ Phecall (odfl `Backward d, s, x) }
31893193

31903194
| EXFALSO
31913195
{ Pexfalso }

‎src/ecParsetree.ml‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -770,6 +770,12 @@ type matchmode = [
770770
(* -------------------------------------------------------------------- *)
771771
type prrewrite = [`Rw of ppterm | `Simpl]
772772

773+
(* -------------------------------------------------------------------- *)
774+
type pecall = pqsymbol * ptyannot option * ppt_arg located list
775+
776+
(* -------------------------------------------------------------------- *)
777+
type pdirection = [`Forward | `Backward]
778+
773779
(* -------------------------------------------------------------------- *)
774780
type phltactic =
775781
| Pskip
@@ -808,7 +814,7 @@ type phltactic =
808814
| Pconcave of (pformula option tuple2 gppterm * pformula)
809815
| Phrex_elim
810816
| Phrex_intro of (pformula list * bool)
811-
| Phecall of (oside * (pqsymbol * ptyannot option * pformula list))
817+
| Phecall of (pdirection * oside * pecall)
812818
| Pexfalso
813819
| Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
814820
| PPr of (pformula * pformula) option

0 commit comments

Comments
 (0)