https://github.com/EasyCrypt/easycrypt
Tip revision: 638f6ed9cce5d6458c8e6230715137a5a663db08 authored by Gustavo Delerue on 28 August 2024, 23:55:14 UTC
WIP: fixed bdep SMT bug
WIP: fixed bdep SMT bug
Tip revision: 638f6ed
ecPhlApp.ml
(* -------------------------------------------------------------------- *)
open EcUtils
open EcLocation
open EcParsetree
open EcTypes
open EcModules
open EcFol
open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal
module TTC = EcProofTyping
(* -------------------------------------------------------------------- *)
let t_hoare_app_r i phi tc =
let env = FApi.tc1_env tc in
let hs = tc1_as_hoareS tc in
let s1, s2 = s_split env i hs.hs_s in
let a = f_hoareS_r { hs with hs_s = stmt s1; hs_po = phi } in
let b = f_hoareS_r { hs with hs_pr = phi; hs_s = stmt s2 } in
FApi.xmutate1 tc `HlApp [a; b]
let t_hoare_app = FApi.t_low2 "hoare-app" t_hoare_app_r
(* -------------------------------------------------------------------- *)
let t_ehoare_app_r i f tc =
let env = FApi.tc1_env tc in
let hs = tc1_as_ehoareS tc in
let s1, s2 = s_split env i hs.ehs_s in
let a = f_eHoareS_r { hs with ehs_s = stmt s1; ehs_po = f } in
let b = f_eHoareS_r { hs with ehs_pr = f; ehs_s = stmt s2 } in
FApi.xmutate1 tc `HlApp [a; b]
let t_ehoare_app = FApi.t_low2 "hoare-app" t_ehoare_app_r
let t_choare_app_r i phi cost tc =
let env = FApi.tc1_env tc in
let chs = tc1_as_choareS tc in
let s1, s2 = s_split env i chs.chs_s in
let cond, cost1 = EcCHoare.cost_sub env chs.chs_co cost in
let a = f_cHoareS_r { chs with chs_s = stmt s1;
chs_po = phi;
chs_co = cost1; } in
let b = f_cHoareS_r { chs with chs_pr = phi;
chs_s = stmt s2;
chs_co = cost; } in
FApi.xmutate1 tc `HlApp [cond; a; b]
let t_choare_app = FApi.t_low3 "choare-app" t_choare_app_r
(* -------------------------------------------------------------------- *)
let t_bdhoare_app_r_low i (phi, pR, f1, f2, g1, g2) tc =
let env = FApi.tc1_env tc in
let bhs = tc1_as_bdhoareS tc in
let s1, s2 = s_split env i bhs.bhs_s in
let s1, s2 = stmt s1, stmt s2 in
let nR = f_not pR in
let cond_phi = f_hoareS bhs.bhs_m bhs.bhs_pr s1 phi in
let condf1 = f_bdHoareS_r { bhs with bhs_s = s1; bhs_po = pR; bhs_bd = f1; } in
let condg1 = f_bdHoareS_r { bhs with bhs_s = s1; bhs_po = nR; bhs_bd = g1; } in
let condf2 = f_bdHoareS_r
{ bhs with bhs_s = s2; bhs_pr = f_and_simpl phi pR; bhs_bd = f2; } in
let condg2 = f_bdHoareS_r
{ bhs with bhs_s = s2; bhs_pr = f_and_simpl phi nR; bhs_bd = g2; } in
let bd =
(f_real_add_simpl (f_real_mul_simpl f1 f2) (f_real_mul_simpl g1 g2)) in
let condbd =
match bhs.bhs_cmp with
| FHle -> f_real_le bd bhs.bhs_bd
| FHeq -> f_eq bd bhs.bhs_bd
| FHge -> f_real_le bhs.bhs_bd bd in
let condbd = f_imp bhs.bhs_pr condbd in
let (ir1, ir2) = EcIdent.create "r", EcIdent.create "r" in
let (r1 , r2 ) = f_local ir1 treal, f_local ir2 treal in
let condnm =
let eqs = f_and (f_eq f2 r1) (f_eq g2 r2) in
f_forall
[(ir1, GTty treal); (ir2, GTty treal)]
(f_hoareS bhs.bhs_m (f_and bhs.bhs_pr eqs) s1 eqs) in
let conds = [f_forall_mems [bhs.bhs_m] condbd; condnm] in
let conds =
if f_equal g1 f_r0
then condg1 :: conds
else if f_equal g2 f_r0
then condg2 :: conds
else condg1 :: condg2 :: conds in
let conds =
if f_equal f1 f_r0
then condf1 :: conds
else if f_equal f2 f_r0
then condf2 :: conds
else condf1 :: condf2 :: conds in
let conds = cond_phi :: conds in
FApi.xmutate1 tc `HlApp conds
(* -------------------------------------------------------------------- *)
let t_bdhoare_app_r i info tc =
let tactic tc =
let hs = tc1_as_hoareS tc in
let tt1 = EcPhlConseq.t_hoareS_conseq_nm hs.hs_pr f_true in
let tt2 = EcPhlAuto.t_pl_trivial in
FApi.t_seqs [tt1; tt2; t_fail] tc
in
FApi.t_last
(FApi.t_try (t_intros_s_seq (`Symbol ["_"; "_"]) tactic))
(t_bdhoare_app_r_low i info tc)
let t_bdhoare_app = FApi.t_low2 "bdhoare-app" t_bdhoare_app_r
(* -------------------------------------------------------------------- *)
let t_equiv_app (i, j) phi tc =
let env = FApi.tc1_env tc in
let es = tc1_as_equivS tc in
let sl1,sl2 = s_split env i es.es_sl in
let sr1,sr2 = s_split env j es.es_sr in
let a = f_equivS_r {es with es_sl=stmt sl1; es_sr=stmt sr1; es_po=phi} in
let b = f_equivS_r {es with es_pr=phi; es_sl=stmt sl2; es_sr=stmt sr2} in
FApi.xmutate1 tc `HlApp [a; b]
let t_equiv_app_onesided side i pre post tc =
let env = FApi.tc1_env tc in
let es = tc1_as_equivS tc in
let m, s, s' =
match side with
| `Left -> es.es_ml, es.es_sl, es.es_sr
| `Right -> es.es_mr, es.es_sr, es.es_sl
in
let ij =
match side with
| `Left -> (i, Zpr.cpos (List.length s'. s_node))
| `Right -> (Zpr.cpos (List.length s'. s_node), i) in
let _s1, s2 = s_split env i s in
let modi = EcPV.s_write env (EcModules.stmt s2) in
let subst = Fsubst.f_subst_mem mhr (fst m) in
let p' = subst pre and q' = subst post in
let r = f_and p' (generalize_mod env (fst m) modi (f_imp q' es.es_po)) in
FApi.t_seqsub (t_equiv_app ij r)
[t_id; (* s1 ~ s' : pr ==> r *)
FApi.t_seqsub (EcPhlConseq.t_equivS_conseq_nm p' q')
[(* r => forall mod, post => post' *) t_trivial;
(* r => p' *) t_trivial;
(* s1 ~ [] : p' ==> q' *) EcPhlConseq.t_equivS_conseq_bd side pre post
]
] tc
(* -------------------------------------------------------------------- *)
let process_phl_c_info app_c_info tc =
match app_c_info with
| PAppCost c -> TTC.tc1_process_cost tc [] c
| PAppSingle _ ->
tc_error !!tc "seq choare: a cost must be supplied, not a bound"
| PAppNone ->
tc_error !!tc "seq choare: a cost must be supplied"
| PAppMult _ ->
tc_error !!tc "seq choare: too many arguments, only a cost must be supplied"
(* -------------------------------------------------------------------- *)
let process_phl_bd_info dir bd_info tc =
match bd_info with
| PAppNone ->
let hs = tc1_as_bdhoareS tc in
let f1, f2 =
match dir with
| Backs -> hs.bhs_bd, f_r1
| Fwds -> f_r1, hs.bhs_bd
in
(* The last argument will not be used *)
(f_true, f1, f2, f_r0, f_r1)
| PAppSingle f ->
let hs = tc1_as_bdhoareS tc in
let f = snd (TTC.tc1_process_Xhl_form tc treal f) in
let f1, f2 =
match dir with
| Backs -> (f_real_div hs.bhs_bd f, f)
| Fwds -> (f, f_real_div hs.bhs_bd f)
in
(f_true, f1, f2, f_r0, f_r1)
| PAppMult (phi, f1, f2, g1, g2) ->
let phi =
phi |> omap (fun f -> snd (TTC.tc1_process_Xhl_formula tc f))
|> odfl f_true in
let check_0 f =
if not (f_equal f f_r0) then
tc_error !!tc "the formula must be 0%%r" in
let process_f (f1,f2) =
match f1, f2 with
| None, None -> assert false
| Some fp, None ->
let _, f = TTC.tc1_process_Xhl_form tc treal fp in
reloc fp.pl_loc check_0 f; (f, f_r1)
| None, Some fp ->
let _, f = TTC.tc1_process_Xhl_form tc treal fp in
reloc fp.pl_loc check_0 f; (f_r1, f)
| Some f1, Some f2 ->
let _, f1 = TTC.tc1_process_Xhl_form tc treal f1 in
let _, f2 = TTC.tc1_process_Xhl_form tc treal f2 in
(f1, f2)
in
let f1, f2 = process_f (f1, f2) in
let g1, g2 = process_f (g1, g2) in
(phi, f1, f2, g1, g2)
| PAppCost _ ->
tc_error !!tc "a cost cannot be supplied here"
(* -------------------------------------------------------------------- *)
let process_app (side, dir, k, phi, bd_info) tc =
let concl = FApi.tc1_goal tc in
let get_single phi =
match phi with
| Single phi -> phi
| Double _ -> tc_error !!tc "seq: a single formula is expected" in
let check_side side =
if EcUtils.is_some side then
tc_error !!tc "seq: no side information expected" in
match k, bd_info with
| Single i, PAppNone when is_hoareS concl ->
check_side side;
let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
t_hoare_app i phi tc
| Single i, PAppNone when is_eHoareS concl ->
check_side side;
let _, phi = TTC.tc1_process_Xhl_formula_xreal tc (get_single phi) in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
t_ehoare_app i phi tc
| Single i, PAppNone when is_equivS concl ->
let pre, post =
match phi with
| Single _ -> tc_error !!tc "seq onsided: a pre and a post is expected"
| Double (pre, post) ->
let _, pre = TTC.tc1_process_Xhl_formula ?side tc pre in
let _, post = TTC.tc1_process_Xhl_formula ?side tc post in
(pre, post) in
let side =
match side with
| None -> tc_error !!tc "seq onsided: side information expected"
| Some side -> side in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
t_equiv_app_onesided side i pre post tc
| Single i, _ when is_cHoareS concl ->
check_side side;
let _, phi = TTC.tc1_process_Xhl_formula tc (get_single phi) in
let cost = process_phl_c_info bd_info tc in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
t_choare_app i phi cost tc
| Single i, _ when is_bdHoareS concl ->
let _, pia = TTC.tc1_process_Xhl_formula tc (get_single phi) in
let (ra, f1, f2, f3, f4) = process_phl_bd_info dir bd_info tc in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
t_bdhoare_app i (ra, pia, f1, f2, f3, f4) tc
| Double (i, j), PAppNone when is_equivS concl ->
let phi = TTC.tc1_process_prhl_formula tc (get_single phi) in
let i = EcTyping.trans_codepos1 (FApi.tc1_env tc) i in
let j = EcTyping.trans_codepos1 (FApi.tc1_env tc) j in
t_equiv_app (i, j) phi tc
| Single _, PAppNone
| Double _, PAppNone ->
tc_error !!tc "invalid `position' parameter"
| _, _ ->
tc_error !!tc "optional bound parameter not supported"