Skip to content

Make abstract phoare proc use a >= 1 #887

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
oskgo wants to merge 1 commit into
base: main
Choose a base branch
from
+17 −4
Open

Make abstract phoare proc use a >= 1 #887

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
21 changes: 17 additions & 4 deletions src/phl/ecPhlFun.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ module FunAbsLow = struct
PV.check_depend env fv top;
let ospec o =
check_oracle_use pf env top o;
f_bdHoareF inv o inv FHeq {m=inv.m;inv=f_r1} in
f_bdHoareF inv o inv FHge {m=inv.m;inv=f_r1} in

let sg = List.map ospec (OI.allowed oi) in
(inv, inv, lossless_hyps env top f.x_sub :: sg)
Expand Down Expand Up @@ -259,19 +259,32 @@ let t_ehoareF_abs_r inv tc =
FApi.t_last tactic (EcPhlConseq.t_ehoareF_conseq pre post tc)

(* ------------------------------------------------------------------ *)
let t_bdhoareF_abs_r inv tc =
let t_bdhoareF_abs_ge_r inv tc =
let env = FApi.tc1_env tc in
let bhf = tc1_as_bdhoareF tc in

match bhf.bhf_cmp with
| FHeq when f_equal (bhf_bd bhf).inv f_r1 ->
| FHge when f_equal (bhf_bd bhf).inv f_r1 ->
let pre, post, sg =
FunAbsLow.bdhoareF_abs_spec !!tc env bhf.bhf_f inv
in
let tactic tc = FApi.xmutate1 tc `FunAbs sg in
FApi.t_last tactic (EcPhlConseq.t_bdHoareF_conseq pre post tc)

| _ -> tc_error !!tc "bound must of \"= 1\""
| _ -> tc_error !!tc "bound must \">= 1%%r\""

let t_bdhoareF_abs_r inv tc =
Copy link
Member

@strub strub Feb 5, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This function seems to be used nowhere.

Copy link
Contributor Author

@oskgo oskgo Feb 6, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The diff might look a bit weird. The function you're highlighting is the original function, which is used to define t_bdhoareF_abs, which is used in a bunch of places.

The t_bdhoareF_abs_ge_r function above is the new one, though its implementation is nearly the same as the original.

let bhf = tc1_as_bdhoareF tc in

match bhf.bhf_cmp with
| FHeq when f_equal (bhf_bd bhf).inv f_r1 ->
let tc = FApi.t_seqsub (EcPhlConseq.t_bdHoareF_conseq_bd FHge (bhf_bd bhf)) [EcLowGoal.t_close EcLowGoal.t_trivial; t_bdhoareF_abs_ge_r inv] tc in
let pl_goal_count = FApi.tc_count tc - 3 in
assert (pl_goal_count >= 0);
FApi.t_lasts (EcPhlConseq.t_bdHoareF_conseq_bd FHeq (bhf_bd bhf) |- FApi.t_first (EcLowGoal.t_close EcLowGoal.t_trivial)) pl_goal_count tc
| FHge when f_equal (bhf_bd bhf).inv f_r1 ->
t_bdhoareF_abs_ge_r inv tc
| _ -> tc_error !!tc "bound must \"= 1%%r\" or \">= 1%%r\""

(* ------------------------------------------------------------------ *)
let t_equivF_abs_r inv tc =
Expand Down