Skip to content

Tactic: add hoare split #888

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
base: main
Choose a base branch
from
+115 −1
Open

Tactic: add hoare split #888

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
73 changes: 73 additions & 0 deletions doc/tactics/hoare-split.rst
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,73 @@
========================================================================
Tactic: `hoare split`
========================================================================

The `hoare split` tactic applies to **Hoare-logic goals only** whose
postcondition is a conjunction.

In this situation, the program is required to establish *all* components of
the postcondition. The `hoare split` tactic makes this explicit by splitting
the original goal into independent Hoare goals, one for each conjunct.

Applying `hoare split` does not modify the program or the precondition. It
only decomposes the logical structure of the postcondition.

.. note::

The `hoare split` tactic is new and subject to change. Its interface and
behavior may evolve in future versions of EasyCrypt.

.. contents::
:local:

------------------------------------------------------------------------
Syntax
------------------------------------------------------------------------

.. admonition:: Syntax

`hoare split`

This tactic takes no arguments. It can be applied whenever the conclusion
of a Hoare goal is a conjunction.

------------------------------------------------------------------------
Example
------------------------------------------------------------------------

.. ecproof::
:title: Splitting a conjunctive postcondition

require import AllCore.

module M = {
proc incr(x : int) : int = {
var y : int;
y <- x + 1;
return y;
}
}.

lemma L (n : int) : 0 <= n =>
hoare [M.incr : x = n ==> n < res /\ 0 <= res].
proof.
move=> ge0_n; proc.

(*$*) (* Split the conjunctive postcondition *)
hoare split.

- (* First conjunct: n < y *)
wp; skip; smt().

- (* Second conjunct: 0 <= y *)
wp; skip; smt().
qed.

------------------------------------------------------------------------
Note
------------------------------------------------------------------------

This tactic is specific to Hoare logic. An analogous transformation would be
unsound in other program logics supported by EasyCrypt (such as probabilistic
or relational program logics), where a conjunctive postcondition does not, in
general, decompose into independent proof obligations.
1 change: 1 addition & 0 deletions src/ecHiTacticals.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -232,6 +232,7 @@ and process1_phl (_ : ttenv) (t : phltactic located) (tc : tcenv1) =
| Pprocrewrite (s, p, f) -> EcPhlRewrite.process_rewrite s p f
| Pchangestmt (s, p, c) -> EcPhlRewrite.process_change_stmt s p c
| Prwprgm infos -> EcPhlRwPrgm.process_rw_prgm infos
| Phoaresplit -> EcPhlHoare.process_hoaresplit
in

try tx tc
Expand Down
3 changes: 3 additions & 0 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3163,6 +3163,9 @@ interleave_info:
| PROC REWRITE side=side? pos=codepos SLASHEQ
{ Pprocrewrite (side, pos, `Simpl) }

| HOARE SPLIT
{ Phoaresplit }

| IDASSIGN o=codepos x=lvalue_var
{ Prwprgm (`IdAssign (o, x)) }

Expand Down
2 changes: 1 addition & 1 deletion src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -773,7 +773,7 @@ type phltactic =
| Prwprgm of rwprgm
| Pprocrewrite of side option * pcodepos * prrewrite
| Pchangestmt of side option * pcodepos_range * pstmt

| Phoaresplit

(* Eager *)
| Peager_seq of (pcodepos1 pair * pstmt * pformula doption)
Expand Down
2 changes: 2 additions & 0 deletions src/phl/ecPhlConseq.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ val t_ehoareS_conseq : ss_inv -> ss_inv -> FApi.backward
val t_bdHoareS_conseq_bd : hoarecmp -> ss_inv -> FApi.backward
val t_bdHoareF_conseq_bd : hoarecmp -> ss_inv -> FApi.backward

val t_hoareS_conseq_conj : ss_inv -> ss_inv -> ss_inv -> ss_inv -> FApi.backward

(* -------------------------------------------------------------------- *)
val t_equivF_conseq_nm : ts_inv -> ts_inv -> FApi.backward
val t_equivS_conseq_nm : ts_inv -> ts_inv -> FApi.backward
Expand Down
29 changes: 29 additions & 0 deletions src/phl/ecPhlHoare.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
(* ------------------------------------------------------------------------ *)
open EcAst
open EcFol
open EcLowPhlGoal
open EcCoreGoal

(* ------------------------------------------------------------------------ *)
let t_hoaresplit (tc : tcenv1) =
let hoare = tc1_as_hoareS tc in
let pre = hs_pr hoare in
let post = 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 = { post with inv = f1 } in
let cr = { post with inv = f2 } 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
6 changes: 6 additions & 0 deletions src/phl/ecPhlHoare.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
(* ------------------------------------------------------------------------ *)
open EcCoreGoal.FApi

(* ------------------------------------------------------------------------ *)
val t_hoaresplit : backward
val process_hoaresplit : backward