Skip to content

Commit cf9b1d9

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 7640b32 commit cf9b1d9

18 files changed

Lines changed: 859 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
@@ -372,6 +372,10 @@ module EV = struct
372372
| Some (`Set _) -> true
373373
| _ -> false
374374

375+
let map (f : 'a -> 'a) (m : 'a evmap) =
376+
{ ev_map = Mid.map (omap f) m.ev_map
377+
; ev_unset = m.ev_unset }
378+
375379
let doget (x : ident) (m : 'a evmap) =
376380
match get x m with
377381
| Some (`Set a) -> a

‎src/ecMatching.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -150,6 +150,7 @@ module EV : sig
150150
val isset : ident -> 'a evmap -> bool
151151
val set : ident -> 'a -> 'a evmap -> 'a evmap
152152
val get : ident -> 'a evmap -> [`Unset | `Set of 'a] option
153+
val map : ('a -> 'a) -> 'a evmap -> 'a evmap
153154
val doget : ident -> 'a evmap -> 'a
154155
val fold : (ident -> 'a -> 'b -> 'b) -> 'a evmap -> 'b -> 'b
155156
val filled : 'a evmap -> bool

‎src/ecPV.ml‎

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

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

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

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

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

633642
(* -------------------------------------------------------------------- *)
634643
type pmvs = PV.t Mid.t

‎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
type pmvs = PV.t EcIdent.Mid.t

‎src/ecParser.mly‎

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

2933+
direction:
2934+
| RRARROW { (`Forward :> pdirection) }
2935+
| LLARROW { (`Backward :> pdirection) }
2936+
29332937
%public phltactic:
29342938
| PROC
29352939
{ Pfun `Def }
@@ -3115,8 +3119,8 @@ interleave_info:
31153119

31163120
{ Phrex_intro (l, b) }
31173121

3118-
| ECALL s=side? x=paren(p=qident tvi=tvars_app? fs=sform* { (p, tvi, fs) })
3119-
{ Phecall (s, x) }
3122+
| ECALL d=direction? s=side? x=paren(p=qident tvi=tvars_app? fs=loc(gpterm_arg)* { (p, tvi, fs) })
3123+
{ Phecall (odfl `Backward d, s, x) }
31203124

31213125
| EXFALSO
31223126
{ Pexfalso }

‎src/ecParsetree.ml‎

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

739+
(* -------------------------------------------------------------------- *)
740+
type pecall = pqsymbol * ptyannot option * ppt_arg located list
741+
742+
(* -------------------------------------------------------------------- *)
743+
type pdirection = [`Forward | `Backward]
744+
739745
(* -------------------------------------------------------------------- *)
740746
type phltactic =
741747
| Pskip
@@ -774,7 +780,7 @@ type phltactic =
774780
| Pconcave of (pformula option tuple2 gppterm * pformula)
775781
| Phrex_elim
776782
| Phrex_intro of (pformula list * bool)
777-
| Phecall of (oside * (pqsymbol * ptyannot option * pformula list))
783+
| Phecall of (pdirection * oside * pecall)
778784
| Pexfalso
779785
| Pbydeno of ([`PHoare | `Equiv | `EHoare ] * (deno_ppterm * bool * pformula option))
780786
| PPr of (pformula * pformula) option

0 commit comments

Comments
 (0)