Skip to content

refactor(pl): if/match/case on the conditional alone, with pushes #1174

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
+2,343 −509
Open

refactor(pl): if/match/case on the conditional alone, with pushes #1174

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
17 changes: 11 additions & 6 deletions src/phl/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -105,11 +105,15 @@ equiv: one side at a time), parameterized by an entry of a catalogue:
("<logic>-transform") re-runs it on the goal's program and compares the
subgoals up to conversion (programs up to alpha-equivalence).

Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`) and
`rmatch` (`EcTrRMatch`). Further entries come with the tactics that use
them. The framed form of `match C k` changes the precondition: it stays a
separate trusted rule of each logic, `t_<logic>_rmatch_framed`
(`Ec<Logic>RMatch`). See `REFACTORING.md` §7f.
Current catalogue: `rndsem` (`EcTrRndSem`), `rcond` (`EcTrRCond`),
`rmatch` (`EcTrRMatch`), `if-push` (`EcTrIfPush`) and `match-push`
(`EcTrMatchPush`), the last two pushing the continuation of a leading
conditional / `match` into its branches. The `if` and `match` tactics are
push + rule on the conditional alone (`Ec<Logic>If`, `Ec<Logic>Match`).
Further entries come with the tactics that use them. The framed form of
`match C k` changes the precondition: it stays a separate trusted rule of
each logic, `t_<logic>_rmatch_framed` (`Ec<Logic>RMatch`). See
`REFACTORING.md` §7f.

## Directory layout

Expand All @@ -125,7 +129,8 @@ src/phl/
Ec<Logic><Rule>: one module per (logic, rule)
transforms/ EcTr<Name>: catalogue entries of the program transformations
ecPl*.ml computations shared by the rules of every logic: EcPlFrame,
EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform
EcPlSp, EcPlWp, EcPlRndSem, EcPlRCond, EcPlTransform,
EcPlMatch
ecPlRecheck.ml checker scaffolding
ecPhl<Tactic>.ml legacy: thin dispatchers and adapters, not-yet-migrated
tactics
Expand Down
21 changes: 17 additions & 4 deletions src/phl/REFACTORING.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -153,7 +153,8 @@ src/phl/
postcondition), EcPlWp (weakest precondition), EcPlRndSem
(semantic sampling), EcPlRCond (deciding a conditional or
a match), EcPlTransform (the transformation catalogue and
its obligations)
its obligations), EcPlMatch (branches of a `match` on
fresh program variables)
ecPlRecheck.ml checker scaffolding
ecPhl<Tactic>.ml legacy: thin dispatchers and adapters, not-yet-migrated
tactics
Expand Down Expand Up @@ -374,11 +375,23 @@ Current catalogue:
- `rmatch` (`EcTrRMatch`, deciding the `match` at a position, the arguments
of the constructor being assigned to fresh program variables; obligation
`OPrefixPost (hd, exists xs, e = C xs)`), used by `match C k` in every
logic (its unframed form, see below).
logic (its unframed form, see below);
- `if-push` (`EcTrIfPush`): `if b then c1 else c2; c` becomes the single
instruction `if b then { c1; c } else { c2; c }`; no obligation;
- `match-push` (`EcTrMatchPush`): `match e with C xs => b ...; c` becomes
the single instruction `match e with C xs => { b; c } ...`; no
obligation. The pattern variables are local identifiers bound in the
branch only: the binders of a branch are renamed apart when they occur
free in `c`, so that `c` is not captured.

The decisions of a conditional or a match are computed by `EcPlRCond`.
Further entries come with the tactics that use them: if/match-push, then
swap, inline, kill/alias/cfold/set and proc rewrite.
The `if` and `match` tactics are push + rule on the conditional alone: they
push the continuation into the branches (when there is one) through the
transformation rule (on each side, for the two-sided equiv forms), then
apply the `if` / `match` rule of their logic (`Ec<Logic>If`,
`Ec<Logic>Match`), stated on the conditional alone. Further entries come
with the tactics that use them: swap, inline, kill/alias/cfold/set and
proc rewrite.

Exception: the framed form of `match C k` (used when the variables of the
discriminant `e` are neither read nor written by the prefix, and the
Expand Down
107 changes: 31 additions & 76 deletions src/phl/ecPhlCase.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,87 +1,42 @@
(* --------------------------------------------------------------------- *)
open EcFol
open EcCoreGoal
open EcLowPhlGoal
open EcAst

(* --------------------------------------------------------------------- *)
let t_hoare_case_r ?(simplify = true) f tc =
let fand = if simplify then f_and_simpl else f_and in
let hs = tc1_as_hoareS tc in
let mt = snd hs.hs_m in
let concl1 =
f_hoareS mt (map_ss_inv2 fand (hs_pr hs) f) hs.hs_s (hs_po hs)
in
let concl2 =
f_hoareS
mt
(map_ss_inv2 fand (hs_pr hs) (map_ss_inv1 f_not f))
hs.hs_s
(hs_po hs)
in
FApi.xmutate1 tc (`HlCase f) [concl1; concl2]

(* --------------------------------------------------------------------- *)
let t_ehoare_case_r ?(simplify = true) f tc =
let _ = simplify in
let hs = tc1_as_ehoareS tc in
let mt = snd hs.ehs_m in
let concl1 = f_eHoareS mt (map_ss_inv2 f_interp_ehoare_form f (ehs_pr hs)) hs.ehs_s (ehs_po hs) in
let concl2 = f_eHoareS mt (map_ss_inv2 f_interp_ehoare_form (map_ss_inv1 f_not f) (ehs_pr hs)) hs.ehs_s (ehs_po hs) in
FApi.xmutate1 tc (`HlCase f) [concl1; concl2]

(* --------------------------------------------------------------------- *)
let t_bdhoare_case_r ?(simplify = true) f tc =
let fand = if simplify then f_and_simpl else f_and in
let bhs = tc1_as_bdhoareS tc in
let mt = snd bhs.bhs_m in
let concl1 = f_bdHoareS mt (map_ss_inv2 fand (bhs_pr bhs) f) bhs.bhs_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
let concl2 = f_bdHoareS mt
(map_ss_inv2 fand (bhs_pr bhs) (map_ss_inv1 f_not f)) bhs.bhs_s (bhs_po bhs) bhs.bhs_cmp (bhs_bd bhs) in
FApi.xmutate1 tc (`HlCase f) [concl1; concl2]
open EcCoreGoal
open EcLowPhlGoal

(* --------------------------------------------------------------------- *)
let t_equiv_case_r ?(simplify = true) f tc =
let fand = if simplify then f_and_simpl else f_and in
let es = tc1_as_equivS tc in
let mtl, mtr = snd es.es_ml, snd es.es_mr in
let concl1 = f_equivS mtl mtr (map_ts_inv2 fand (es_pr es) f) es.es_sl es.es_sr (es_po es) in
let concl2 = f_equivS mtl mtr (map_ts_inv2 fand (es_pr es) (map_ts_inv1 f_not f)) es.es_sl es.es_sr (es_po es) in
FApi.xmutate1 tc (`HlCase f) [concl1; concl2]
(* The [case] rules live, one module per logic, in [rules/<logic>/]. This
module only keeps the legacy positional entry points (adapters onto
those rules, so that external callers and this module's interface are
unchanged) and the logic-agnostic dispatcher. *)

(* --------------------------------------------------------------------- *)
let t_hoare_case ?simplify =
FApi.t_low1 "hoare-case" (t_hoare_case_r ?simplify)
let t_hoare_case ?(simplify = true) f =
EcHoareCase.(t_hoare_case { hca_cond = f; hca_simplify = simplify })

let t_ehoare_case ?simplify =
FApi.t_low1 "ehoare-case" (t_ehoare_case_r ?simplify)
let t_bdhoare_case ?(simplify = true) f =
EcBdHoareCase.(t_bdhoare_case { bca_cond = f; bca_simplify = simplify })

let t_bdhoare_case ?simplify =
FApi.t_low1 "bdhoare-case" (t_bdhoare_case_r ?simplify)

let t_equiv_case ?simplify =
FApi.t_low1 "equiv-case" (t_equiv_case_r ?simplify)
let t_equiv_case ?(simplify = true) f =
EcEquivCase.(t_equiv_case { eca_cond = f; eca_simplify = simplify })

(* --------------------------------------------------------------------- *)
let t_hl_case_r ?simplify f tc =
match f with
| Inv_ss f ->
t_hS_or_bhS_or_eS
~th:(t_hoare_case ?simplify f)
~teh:(t_ehoare_case ?simplify f)
~tbh:(t_bdhoare_case ?simplify f)
~te:(fun _ -> tc_error !!tc "expecting a two sided formula")
tc
| Inv_ts f ->
let err _ =
tc_error !!tc "expecting a one sided formula" in
t_hS_or_bhS_or_eS
~th:err
~teh:err
~tbh:err
~te:(t_equiv_case ?simplify f)
tc
| _ -> assert false

(* -------------------------------------------------------------------- *)
let t_hl_case ?simplify = FApi.t_low1 "hl-case" (t_hl_case_r ?simplify)
(* Dispatch on the formula kind and the goal kind. The ehoare rule has no
[simplify] option: its precondition is not a conjunction. *)
let t_hl_case ?simplify f tc =
match f, (FApi.tc1_goal tc).f_node with
| Inv_hs _, _ -> assert false

| Inv_ss f, FhoareS _ -> t_hoare_case ?simplify f tc
| Inv_ss f, FeHoareS _ -> EcEHoareCase.(t_ehoare_case { ehca_cond = f }) tc
| Inv_ss f, FbdHoareS _ -> t_bdhoare_case ?simplify f tc
| Inv_ss _, FequivS _ -> tc_error !!tc "expecting a two sided formula"

| Inv_ts f, FequivS _ -> t_equiv_case ?simplify f tc
| Inv_ts _, (FhoareS _ | FeHoareS _ | FbdHoareS _) ->
tc_error !!tc "expecting a one sided formula"

| _, _ ->
tc_error_noXhl
~kinds:[`Hoare `Stmt; `EHoare `Stmt; `PHoare `Stmt; `Equiv `Stmt]
!!tc
Loading
Loading