Skip to content

refactor(pl): pr bridges as recheckable per-logic rules #1165

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

Open
strub wants to merge 1 commit into from
+1,372 −448
Open

refactor(pl): pr bridges as recheckable per-logic rules #1165

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
9 changes: 9 additions & 0 deletions src/ecLowPhlGoal.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -379,6 +379,15 @@ let hs_observes_exn (po : hs_inv) =
(fun _ f -> not (f_equal (snd (decompose_lambda f)) f_true))
po.hsi_inv.exnmap

(* -------------------------------------------------------------------- *)
(* The argument of a call to [fun_], as passed to [Pr[fun_(...) @ &m : _]],
read off [arg], the value of its (tuple) argument variable. *)
let pr_args_of_fun (fun_ : function_) (arg : form) =
match fun_.f_sig.fs_anames with
| [] -> f_tt
| [_] -> arg
| lv -> f_tuple (List.mapi (fun i v -> f_proj arg i v.ov_type) lv)

(* -------------------------------------------------------------------- *)
type logicS = [
| `Hoare of sHoareS
Expand Down
180 changes: 16 additions & 164 deletions src/phl/ecPhlBdHoare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,175 +1,27 @@
(* -------------------------------------------------------------------- *)
open EcAst
open EcFol

open EcCoreGoal
open EcLowGoal
open EcLowPhlGoal

open EcPhlCoreView
open EcPhlConseq

module TTC = EcProofTyping

(* -------------------------------------------------------------------- *)
(* The top-level tactic *)
let t_hoare_bd_hoare tc =
let concl = FApi.tc1_goal tc in

match concl.f_node with
| FbdHoareF bhf ->
if bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0
then t_hoare_of_bdhoareF tc
else
FApi.t_seqsub
(t_bdHoareF_conseq_bd FHeq {m=bhf.bhf_m; inv=f_r0})
[FApi.t_try EcPhlAuto.t_pl_trivial; t_hoare_of_bdhoareF]
tc

| FbdHoareS bhs ->
if bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0
then t_hoare_of_bdhoareS tc
else
FApi.t_seqsub
(t_bdHoareS_conseq_bd FHeq {m=fst bhs.bhs_m; inv=f_r0})
[FApi.t_try EcPhlAuto.t_pl_trivial; t_hoare_of_bdhoareS]
tc

| FhoareF _ -> t_bdhoare_of_hoareF tc
| FhoareS _ -> t_bdhoare_of_hoareS tc

| _ -> tc_error !!tc "a hoare or phoare judgment was expected"

(* -------------------------------------------------------------------- *)
type 'a split_t = {
as_bdh : proofenv -> form -> 'a * ss_inv * hoarecmp * ss_inv;
mk_bdh : 'a * ss_inv * hoarecmp * ss_inv -> form;
}

type 'a destr_t = {
as_bop : proofenv -> ss_inv -> ss_inv * ss_inv;
mk_bop : ss_inv -> ss_inv -> ss_inv;
}

(* -------------------------------------------------------------------- *)
let t_bdhoare_split_bop sp dt b1 b2 b3 tc =
let concl = FApi.tc1_goal tc in
let bh, po, cmp, bd = sp.as_bdh !!tc concl in
let a, b = dt.as_bop !!tc po in

let g1 = sp.mk_bdh (bh, a, cmp, b1) in
let g2 = sp.mk_bdh (bh, b, cmp, b2) in
let g3 = sp.mk_bdh (bh, dt.mk_bop a b, hoarecmp_opp cmp, b3) in
let nb = map_ss_inv2 f_real_sub (map_ss_inv2 f_real_add b1 b2) b3 in

assert (f_equal nb.inv bd.inv);
FApi.xmutate1 tc `BdHoareSplit [g1; g2; g3]

(* -------------------------------------------------------------------- *)
let t_bdhoare_split_bop_conseq t_conseq_bd sp dt b1 b2 b3 tc =
let concl = FApi.tc1_goal tc in
let _, _, cmp, b = sp.as_bdh !!tc concl in
let nb = map_ss_inv2 f_real_sub (map_ss_inv2 f_real_add b1 b2) b3 in
let t_main = t_bdhoare_split_bop sp dt b1 b2 b3 in

if f_equal nb.inv b.inv
then t_main tc
else FApi.t_seqsub (t_conseq_bd cmp nb) [t_id; t_main] tc

(* -------------------------------------------------------------------- *)
let bdhoare_kind tc =
(* The rules behind the [hoare] tactic (views between hoare and
probability-0 bdhoare judgements) and the bdhoare [split] rules live in
[rules/<logic>/]. This module only keeps the dispatcher and the legacy
positional entry points. *)
let t_hoare_bd_hoare (tc : tcenv1) =
match (FApi.tc1_goal tc).f_node with
| FbdHoareS _ -> true
| FbdHoareF _ -> false
| _ -> tc_error !!tc "the conclusion should be a bdhoare judgment"

(* -------------------------------------------------------------------- *)
let gen_S tactic =
let as_bdh pf f =
let bh = pf_as_bdhoareS pf f in
(bh, (bhs_po bh), bh.bhs_cmp, bhs_bd bh)

and mk_bdh (bh, po, cmp, b) =
f_bdHoareS (snd bh.bhs_m) (bhs_pr bh) bh.bhs_s po cmp b in

tactic t_bdHoareS_conseq_bd { as_bdh; mk_bdh; }

(* -------------------------------------------------------------------- *)
let gen_F tactic =
let as_bdh pf f =
let bh = pf_as_bdhoareF pf f in
(bh, (bhf_po bh), bh.bhf_cmp, bhf_bd bh) in

let mk_bdh (bh, po, cmp, b) =
f_bdHoareF (bhf_pr bh) bh.bhf_f po cmp b in

tactic t_bdHoareF_conseq_bd { as_bdh; mk_bdh; }

(* -------------------------------------------------------------------- *)
let and_dt =
let destr_and pf f =
try
let f1 = map_ss_inv1 (fun f -> fst (destr_and f)) f in
let f2 = map_ss_inv1 (fun f -> snd (destr_and f)) f in
(f1, f2)
with DestrError _ ->
tc_error pf "the postcondition must be a conjunction"
in
{ as_bop = destr_and; mk_bop = map_ss_inv2 f_or; }

let t_bdhoareS_and = gen_S t_bdhoare_split_bop_conseq and_dt
let t_bdhoareF_and = gen_F t_bdhoare_split_bop_conseq and_dt

let t_bdhoare_and b1 b2 b3 tc =
if bdhoare_kind tc
then t_bdhoareS_and b1 b2 b3 tc
else t_bdhoareF_and b1 b2 b3 tc

(* -------------------------------------------------------------------- *)
let or_dt =
let destr_or pf f =
try
let f1 = map_ss_inv1 (fun f -> fst (destr_or f)) f in
let f2 = map_ss_inv1 (fun f -> snd (destr_or f)) f in
(f1, f2)
with DestrError _ ->
tc_error pf "the postcondition must be a disjunction"
in
{ as_bop = destr_or; mk_bop = map_ss_inv2 f_and; }

let t_bdhoareS_or = gen_S t_bdhoare_split_bop_conseq or_dt
let t_bdhoareF_or = gen_F t_bdhoare_split_bop_conseq or_dt

let t_bdhoare_or b1 b2 b3 tc =
if bdhoare_kind tc
then t_bdhoareS_or b1 b2 b3 tc
else t_bdhoareF_or b1 b2 b3 tc
| FbdHoareF _ -> EcBdHoareOfHoare.t_bdhoareF_of_hoare_full tc
| FbdHoareS _ -> EcBdHoareOfHoare.t_bdhoareS_of_hoare_full tc
| FhoareF _ -> EcHoareOfBdHoare.t_hoareF_of_bdhoare tc
| FhoareS _ -> EcHoareOfBdHoare.t_hoareS_of_bdhoare tc
| _ -> tc_error !!tc "a hoare or phoare judgment was expected"

(* -------------------------------------------------------------------- *)
let t_bdhoare_split_not split b1 b2 tc =
let bh, po, cmp, bd = split.as_bdh !!tc (FApi.tc1_goal tc) in
let g1 = split.mk_bdh (bh, map_ss_inv1 (fun _ -> f_true) po, cmp, b1) in
let g2 = split.mk_bdh (bh, map_ss_inv1 f_not_simpl po, hoarecmp_opp cmp, b2) in
let nb = map_ss_inv2 f_real_sub b1 b2 in

assert (f_equal nb.inv bd.inv);
FApi.xmutate1 tc `BdHoareSplit [g1; g2]

let t_bdhoare_split_not_conseq t_conseq_bd split b1 b2 tc =
let hyps = FApi.tc1_hyps tc in
let _, _, cmp, b = split.as_bdh !!tc (FApi.tc1_goal tc) in
let nb = map_ss_inv2 f_real_sub b1 b2 in
let t_main = t_bdhoare_split_not split b1 b2 in
let t_bdhoare_and b1 b2 b3 =
EcBdHoareSplit.(t_bdhoare_split_and { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3; })

if EcReduction.ss_inv_alpha_eq hyps nb b
then t_main tc
else FApi.t_seqsub (t_conseq_bd cmp nb) [t_id; t_main] tc

(* -------------------------------------------------------------------- *)
let t_bdhoareS_not = gen_S t_bdhoare_split_not_conseq
let t_bdhoareF_not = gen_F t_bdhoare_split_not_conseq
let t_bdhoare_or b1 b2 b3 =
EcBdHoareSplit.(t_bdhoare_split_or { bsb_b1 = b1; bsb_b2 = b2; bsb_b3 = b3; })

let t_bdhoare_not b1 b2 tc =
if bdhoare_kind tc
then t_bdhoareS_not b1 b2 tc
else t_bdhoareF_not b1 b2 tc
let t_bdhoare_not b1 b2 =
EcBdHoareSplit.(t_bdhoare_split_not { bnt_b1 = b1; bnt_b2 = b2; })
73 changes: 9 additions & 64 deletions src/phl/ecPhlCoreView.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,65 +1,10 @@
(* -------------------------------------------------------------------- *)
open EcFol

open EcCoreGoal
open EcLowPhlGoal
open EcAst

(* -------------------------------------------------------------------- *)
let t_hoare_of_bdhoareS_r tc =
let bhs = tc1_as_bdhoareS tc in
if not (bhs.bhs_cmp = FHeq && f_equal (bhs_bd bhs).inv f_r0) then
tc_error !!tc "%s" "bound must be equal to 0%r";
let post = (map_ss_inv1 f_not (bhs_po bhs)) in
let concl =
f_hoareS (
snd bhs.bhs_m)
(bhs_pr bhs)
bhs.bhs_s
{ hsi_m = post.m; hsi_inv = POE.empty post.inv; }
in
FApi.xmutate1 tc `ViewBdHoare [concl]

(* -------------------------------------------------------------------- *)
let t_hoare_of_bdhoareF_r tc =
let bhf = tc1_as_bdhoareF tc in
if not (bhf.bhf_cmp = FHeq && f_equal (bhf_bd bhf).inv f_r0) then
tc_error !!tc "%s" "bound must be equal to 0%r";
let post = map_ss_inv1 f_not (bhf_po bhf) in
let concl =
f_hoareF
(bhf_pr bhf) bhf.bhf_f
{ hsi_m = post.m; hsi_inv = POE.empty post.inv; }
in
FApi.xmutate1 tc `ViewBdHoare [concl]

(* -------------------------------------------------------------------- *)
let t_bdhoare_of_hoareS_r tc =
let hs = tc1_as_hoareS tc in
let { main = inv } as post = (hs_po hs).hsi_inv in
if not (POE.is_empty post) then
tc_error !!tc "Exceptions are not permitted";
let m = (hs_po hs).hsi_m in
let concl =
f_bdHoareS
(snd hs.hs_m) (hs_pr hs) hs.hs_s
(map_ss_inv1 f_not {m;inv}) FHeq { m = fst hs.hs_m; inv = f_r0; }
in
FApi.xmutate1 tc `ViewBdHoare [concl]

(* -------------------------------------------------------------------- *)
let t_bdhoare_of_hoareF_r tc =
let hf = tc1_as_hoareF tc in
let { main = inv } as post = (hf_po hf).hsi_inv in
if not (POE.is_empty post) then
tc_error !!tc "Exceptions are not permitted";
let m = (hf_po hf).hsi_m in
let concl =
f_bdHoareF (hf_pr hf) hf.hf_f (map_ss_inv1 f_not {m;inv}) FHeq {m=hf.hf_m;inv=f_r0} in
FApi.xmutate1 tc `ViewBdHoare [concl]

(* -------------------------------------------------------------------- *)
let t_hoare_of_bdhoareS = FApi.t_low0 "hoare-bdhoareS" t_hoare_of_bdhoareS_r
let t_hoare_of_bdhoareF = FApi.t_low0 "hoare-bdhoareF" t_hoare_of_bdhoareF_r
let t_bdhoare_of_hoareS = FApi.t_low0 "bdhoare-hoareS" t_bdhoare_of_hoareS_r
let t_bdhoare_of_hoareF = FApi.t_low0 "bdhoare-hoareF" t_bdhoare_of_hoareF_r
(* The views between hoare and probability-0 bdhoare judgements live in
[rules/hoare/ecHoareOfBdHoare] (a hoare goal from a bdhoare premise)
and [rules/bdhoare/ecBdHoareOfHoare] (a bdhoare goal from a hoare
premise). This module only keeps the legacy entry points, named after
the goal they turn into: [t_hoare_of_bdhoare*] acts on a bdhoare goal. *)
let t_hoare_of_bdhoareS = EcBdHoareOfHoare.t_bdhoareS_of_hoare
let t_hoare_of_bdhoareF = EcBdHoareOfHoare.t_bdhoareF_of_hoare
let t_bdhoare_of_hoareS = EcHoareOfBdHoare.t_hoareS_of_bdhoare
let t_bdhoare_of_hoareF = EcHoareOfBdHoare.t_hoareF_of_bdhoare
79 changes: 3 additions & 76 deletions src/phl/ecPhlHiBdHoare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,77 +1,4 @@
(* -------------------------------------------------------------------- *)
open EcUtils
open EcTypes
open EcFol
open EcAst

open EcCoreGoal
open EcLowGoal

module TTC = EcProofTyping

(* -------------------------------------------------------------------- *)
let process_bdhoare_split info tc =
let _, concl = FApi.tc1_flat tc in

let pr, po =
match concl.f_node with
| FbdHoareS bhs ->
(bhs_pr bhs, bhs_po bhs)

| FbdHoareF bhf ->
(bhf_pr bhf, bhf_po bhf)

| _ ->
tc_error !!tc "the conclusion must be a bdhoare judgment" in

match info with
| EcParsetree.BDH_split_bop (b1, b2, b3) ->
let t =
if is_and po.inv then EcPhlBdHoare.t_bdhoare_and
else if is_or po.inv then EcPhlBdHoare.t_bdhoare_or
else
tc_error !!tc
"the postcondition must be a conjunction or a disjunction"
in
let _,b1 = TTC.tc1_process_Xhl_form tc treal b1 in
let _,b2 = TTC.tc1_process_Xhl_form tc treal b2 in
let b3 = b3 |> omap (fun f -> snd ( TTC.tc1_process_Xhl_form tc treal f)) |> odfl {m=b1.m;inv=f_r0} in

t b1 b2 b3 tc

| EcParsetree.BDH_split_or_case (b1, b2, f) ->
let _, b1 = TTC.tc1_process_Xhl_form tc treal b1 in
let _, b2 = TTC.tc1_process_Xhl_form tc treal b2 in
let _, f = TTC.tc1_process_Xhl_formula tc f in

let t_conseq po lemma tactic =
let rwtt tc =
let pt = ptglobal ~tys:[] lemma in

let rwtt = [
EcLowGoal.t_intros_i [EcIdent.create "_"];
EcHiGoal.LowRewrite.t_rewrite (`LtoR, None, None) pt;
t_true;
] in FApi.t_seqs rwtt tc
in

FApi.t_seqsub
(EcPhlConseq.t_conseq (Inv_ss pr) (Inv_ss po))
[t_true; rwtt; tactic]
in

t_conseq
(map_ss_inv2 f_or (map_ss_inv2 f_and f po) (map_ss_inv2 f_and (map_ss_inv1 f_not f) po))
(EcCoreLib.CI_Logic.mk_logic "orDandN")
(FApi.t_on1seq 3
(EcPhlBdHoare.t_bdhoare_or b1 b2 {m=b1.m;inv=f_r0})
(t_conseq
{inv=f_false;m=b1.m}
(EcCoreLib.CI_Logic.mk_logic "andDorN")
EcHiGoal.process_trivial))
tc

| EcParsetree.BDH_split_not (b1, b2) ->
let _,b2 = TTC.tc1_process_Xhl_form tc treal b2 in
let b1 = b1 |> omap (fun f -> snd (TTC.tc1_process_Xhl_form tc treal f)) |> odfl {m=b2.m;inv=f_r1} in
EcPhlBdHoare.t_bdhoare_not b1 b2 tc
(* The elaboration of [phoare split] lives in [rules/bdhoare/ecBdHoareSplit].
This module only keeps the legacy entry point. *)
let process_bdhoare_split = EcBdHoareSplit.process_bdhoare_split
32 changes: 4 additions & 28 deletions src/phl/ecPhlHoare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,30 +1,6 @@
(* ------------------------------------------------------------------------ *)
open EcUtils
open EcAst
open EcFol
open EcLowPhlGoal
open EcCoreGoal
(* Splitting a hoare postcondition lives in [rules/hoare/ecHoareSplit]. This
module only keeps the legacy entry points. *)
let t_hoaresplit = EcHoareSplit.t_hoare_split

(* ------------------------------------------------------------------------ *)
let t_hoaresplit (tc : tcenv1) =
let hoare = tc1_as_hoareS tc in
let pre = hs_pr hoare in
let post = POE.lower (hs_po hoare) in

match sform_of_form post.inv with
| SFand (`Sym, (f1, f2)) ->
let dp = map_ss_inv2 f_and pre pre in
let cl = update_hs_ss { post with inv = f1 } (hs_po hoare) in
let cr = update_hs_ss { post with inv = f2 } (hs_po hoare) in

EcPhlConseq.t_hoareS_conseq dp (hs_po hoare) tc
|> FApi.t_firsts EcHiGoal.process_done 2
|> FApi.as_tcenv1
|> EcPhlConseq.t_hoareS_conseq_conj (hs_pr hoare) cr (hs_pr hoare) cl

| _ ->
tc_error !!tc "post-condition should be a conjunction"

(* ------------------------------------------------------------------------ *)
let process_hoaresplit (tc : tcenv1) =
t_hoaresplit tc
let process_hoaresplit = EcHoareSplit.t_hoare_split
Loading
Loading