Skip to content
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

Add tactic for lossless while #669

Draft
wants to merge 2 commits into
base: main
Choose a base branch
from
Draft

Add tactic for lossless while #669

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4fc93e8
Add one side while rule with lossless
lyonel2017 Nov 25, 2024
0173967
Some refactoring
lyonel2017 Dec 11, 2024
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
252 changes: 155 additions & 97 deletions src/phl/ecPhlWhile.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -339,6 +339,149 @@ let t_equiv_while_disj_r side vrnt inv tc =

FApi.xmutate1 tc `While [b_concl; concl]

(* -------------------------------------------------------------------- *)
module LossLess = struct
exception CannotTranslate

let form_of_expr env mother mh =
let map = ref (Mid.add mother (EcPV.PVMap.create env) Mid.empty) in

let rec aux fp =
match fp.f_node with
| Fint z -> e_int z
| Flocal x -> e_local x fp.f_ty

| Fop (p, tys) -> e_op p tys fp.f_ty
| Fapp (f, fs) -> e_app (aux f) (List.map aux fs) fp.f_ty
| Ftuple fs -> e_tuple (List.map aux fs)
| Fproj (f, i) -> e_proj (aux f) i fp.f_ty

| Fif (c, f1, f2) ->
e_if (aux c) (aux f1) (aux f2)

| Fmatch (c, bs, ty) ->
e_match (aux c) (List.map aux bs) ty

| Flet (lp, f1, f2) ->
e_let lp (aux f1) (aux f2)

| Fquant (kd, bds, f) ->
e_quantif (auxkd kd) (List.map auxbd bds) (aux f)

| Fpvar (pv, m) ->
if EcIdent.id_equal m mh then
e_var pv fp.f_ty
else
let bds = odfl (EcPV.PVMap.create env) (Mid.find_opt m !map) in
let idx =
match EcPV.PVMap.find pv bds with
| None ->
let pfx = EcIdent.name m in
let pfx = String.sub pfx 1 (String.length pfx - 1) in
let x = symbol_of_pv pv in
let x = EcIdent.create (x ^ "_" ^ pfx) in
let bds = EcPV.PVMap.add pv (x, fp.f_ty) bds in
map := Mid.add m bds !map; x
| Some (x, _) -> x

in e_local idx fp.f_ty

| Fglob _
| FhoareF _ | FhoareS _
| FeHoareF _ | FeHoareS _
| FbdHoareF _ | FbdHoareS _
| FequivF _ | FequivS _
| FeagerF _ | Fpr _ -> raise CannotTranslate

and auxkd (kd : quantif) : equantif =
match kd with
| Lforall -> `EForall
| Lexists -> `EExists
| Llambda -> `ELambda

and auxbd ((x, bd) : binding) =
match bd with
| GTty ty -> (x, ty)
| _ -> raise CannotTranslate

in fun f -> let e = aux f in (e, !map)

let xhyps evs =
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in

fun m fp ->
let fp =
Mid.fold (fun mh pvs fp ->
let mty = Mid.find_opt mh mtypes in
let fp =
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
f_let1 x (f_pvar pv ty mh) fp)
(EcPV.PVMap.raw pvs) fp
in f_forall_mems [mh, oget mty] fp)
m fp
and cnt =
Mid.fold
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
m 0
in (cnt, fp)
end

(* -------------------------------------------------------------------- *)
let t_equiv_ll_while_disj_r side inv tc =
let env = FApi.tc1_env tc in
let es = tc1_as_equivS tc in
let s, m_side, m_other =
match side with
| `Left -> es.es_sl, es.es_ml, es.es_mr
| `Right -> es.es_sr, es.es_mr, es.es_ml in
let (e, c), s = tc1_last_while tc s in
let e = form_of_expr (EcMemory.memory m_side) e in

let (_,ll) =
try
let evs = tc1_as_equivS tc in
let ml = EcMemory.memory evs.es_ml in
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
let inv = Fsubst.f_subst subst inv in
let e, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml e in
let c = s_while (e, c) in
LossLess.xhyps evs m
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)
with LossLess.CannotTranslate ->
tc_error !!tc
"while linking predicates cannot be converted to expressions" in

(* 1. The body preserves the invariant and the loop is lossless. *)

let m_other' = (EcIdent.create "&m", EcMemory.memtype m_other) in

let smem = Fsubst.f_subst_id in
let smem = Fsubst.f_bind_mem smem (EcMemory.memory m_side ) mhr in
let smem = Fsubst.f_bind_mem smem (EcMemory.memory m_other) (EcMemory.memory m_other') in

let b_pre = f_and_simpl inv e in
let b_pre = Fsubst.f_subst smem b_pre in
let b_post = inv in
let b_post = Fsubst.f_subst smem b_post in
let b_concl = f_bdHoareS (mhr, EcMemory.memtype m_side) b_pre c b_post FHeq f_r1 in
let b_concl = b_concl in
let b_concl = f_forall_mems [m_other'] b_concl in

(* 2. WP of the while *)
let post = f_imps_simpl [f_not_simpl e; inv] es.es_po in
let term_condition = f_imps_simpl [inv] (f_not_simpl e) in
let post = f_and term_condition post in
let modi = s_write env c in
let post = generalize_mod env (EcMemory.memory m_side) modi post in
let post = f_and_simpl inv post in
let concl =
match side with
| `Left -> f_equivS_r { es with es_sl = s; es_po=post; }
| `Right -> f_equivS_r { es with es_sr = s; es_po=post; }
in

FApi.xmutate1 tc `While [b_concl; ll; concl]

(* -------------------------------------------------------------------- *)
let t_equiv_while_r inv tc =
let env = FApi.tc1_env tc in
Expand Down Expand Up @@ -374,6 +517,7 @@ let t_bdhoare_while_rev_geq = FApi.t_low4 "bdhoare-while" t_bdhoare_while_rev_ge
let t_bdhoare_while_rev = FApi.t_low1 "bdhoare-while" t_bdhoare_while_rev_r
let t_equiv_while = FApi.t_low1 "equiv-while" t_equiv_while_r
let t_equiv_while_disj = FApi.t_low3 "equiv-while" t_equiv_while_disj_r
let t_equiv_ll_while_dish = FApi.t_low2 "equiv-while" t_equiv_ll_while_disj_r

(* -------------------------------------------------------------------- *)
let process_while side winfos tc =
Expand All @@ -400,7 +544,6 @@ let process_while side winfos tc =
| Some vrnt, None ->
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
let _, vrnt = TTC.tc1_process_Xhl_form tc tint vrnt in

t_bdhoare_while phi vrnt tc

| Some vrnt, Some (`Bd (k, eps)) ->
Expand All @@ -410,7 +553,6 @@ let process_while side winfos tc =
let _, eps = TTC.tc1_process_Xhl_form tc treal eps in

t_bdhoare_while_rev_geq phi vrnt k eps tc

| None, None ->
let _, phi = TTC.tc1_process_Xhl_formula tc phi in
t_bdhoare_while_rev phi tc
Expand All @@ -430,79 +572,16 @@ let process_while side winfos tc =
(TTC.tc1_process_prhl_formula tc phi)
tc

| Some side, None ->
t_equiv_ll_while_dish side
(TTC.tc1_process_prhl_formula tc phi)
tc

| _ -> tc_error !!tc "invalid arguments"
end

| _ -> tc_error !!tc "expecting a hoare[...]/equiv[...]"

(* -------------------------------------------------------------------- *)
module ASyncWhile = struct
exception CannotTranslate

let form_of_expr env mother mh =
let map = ref (Mid.add mother (EcPV.PVMap.create env) Mid.empty) in

let rec aux fp =
match fp.f_node with
| Fint z -> e_int z
| Flocal x -> e_local x fp.f_ty

| Fop (p, tys) -> e_op p tys fp.f_ty
| Fapp (f, fs) -> e_app (aux f) (List.map aux fs) fp.f_ty
| Ftuple fs -> e_tuple (List.map aux fs)
| Fproj (f, i) -> e_proj (aux f) i fp.f_ty

| Fif (c, f1, f2) ->
e_if (aux c) (aux f1) (aux f2)

| Fmatch (c, bs, ty) ->
e_match (aux c) (List.map aux bs) ty

| Flet (lp, f1, f2) ->
e_let lp (aux f1) (aux f2)

| Fquant (kd, bds, f) ->
e_quantif (auxkd kd) (List.map auxbd bds) (aux f)

| Fpvar (pv, m) ->
if EcIdent.id_equal m mh then
e_var pv fp.f_ty
else
let bds = odfl (EcPV.PVMap.create env) (Mid.find_opt m !map) in
let idx =
match EcPV.PVMap.find pv bds with
| None ->
let pfx = EcIdent.name m in
let pfx = String.sub pfx 1 (String.length pfx - 1) in
let x = symbol_of_pv pv in
let x = EcIdent.create (x ^ "_" ^ pfx) in
let bds = EcPV.PVMap.add pv (x, fp.f_ty) bds in
map := Mid.add m bds !map; x
| Some (x, _) -> x

in e_local idx fp.f_ty

| Fglob _
| FhoareF _ | FhoareS _
| FeHoareF _ | FeHoareS _
| FbdHoareF _ | FbdHoareS _
| FequivF _ | FequivS _
| FeagerF _ | Fpr _ -> raise CannotTranslate

and auxkd (kd : quantif) : equantif =
match kd with
| Lforall -> `EForall
| Lexists -> `EExists
| Llambda -> `ELambda

and auxbd ((x, bd) : binding) =
match bd with
| GTty ty -> (x, ty)
| _ -> raise CannotTranslate

in fun f -> let e = aux f in (e, !map)
end

(* -------------------------------------------------------------------- *)
let process_async_while (winfos : EP.async_while_info) tc =
let e_and e1 e2 =
Expand Down Expand Up @@ -587,52 +666,31 @@ let process_async_while (winfos : EP.async_while_info) tc =
in (hr1, hr2)
in

let xhyps =
let mtypes = Mid.of_list [evs.es_ml; evs.es_mr] in

fun m fp ->
let fp =
Mid.fold (fun mh pvs fp ->
let mty = Mid.find_opt mh mtypes in
let fp =
EcPV.Mnpv.fold (fun pv (x, ty) fp ->
f_let1 x (f_pvar pv ty mh) fp)
(EcPV.PVMap.raw pvs) fp
in f_forall_mems [mh, oget mty] fp)
m fp
and cnt =
Mid.fold
(fun _ pvs i -> i + 1 + EcPV.Mnpv.cardinal (EcPV.PVMap.raw pvs))
m 0
in (cnt, fp)
in

let (c1, ll1), (c2, ll2) =
try
let ll1 =
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id ml mhr in
let inv = Fsubst.f_subst subst inv in
let test = f_ands [fe1; f_not p0; p1] in
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_mr) ml test in
let c = s_while (test, cl) in
xhyps m
LossLess.xhyps evs m
(f_bdHoareS (mhr, EcMemory.memtype evs.es_ml) inv c f_true FHeq f_r1)

and ll2 =
let subst = Fsubst.f_bind_mem Fsubst.f_subst_id mr mhr in
let inv = Fsubst.f_subst subst inv in
let test = f_ands [fe1; f_not p0; f_not p1] in
let test, m = ASyncWhile.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
let test, m = LossLess.form_of_expr env (EcMemory.memory evs.es_ml) mr test in
let c = s_while (test, cr) in
xhyps m
LossLess.xhyps evs m
(f_bdHoareS (mhr, EcMemory.memtype evs.es_mr) inv c f_true FHeq f_r1)

in (ll1, ll2)

with ASyncWhile.CannotTranslate ->
with LossLess.CannotTranslate ->
tc_error !!tc
"async-while linking predicates cannot be converted to expressions"
in
"async-while linking predicates cannot be converted to expressions" in

let concl =
let post = f_imps [f_not fe1; f_not fe2; inv] evs.es_po in
Expand Down