Skip to content

Commit 6429f26

Browse files
github-actions[bot]github-actions[bot]
committed
1 parent c48d1e0 commit 6429f26

10 files changed

Lines changed: 1314 additions & 5 deletions

File tree

‎refman/_sources/tactics/proc.rst.txt‎

Lines changed: 383 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,383 @@
1+
========================================================================
2+
Tactic: ``proc``
3+
========================================================================
4+
5+
The ``proc`` tactic applies to program-logic goals where the procedure(s)
6+
under consideration are referred to by name rather than content. It is
7+
typically the first tactic applied when reasoning about procedure calls
8+
or top level program logic statements.
9+
10+
There are two variants of the ``proc`` tactic, depending on whether the
11+
procedure(s) in question are abstract (i.e., declared but not defined)
12+
or concrete (i.e., defined with a body of code).
13+
14+
The abstract variant is a bit different for probabilistic relational
15+
Hoare logic compared to the other program logics, so we describe it
16+
separately.
17+
18+
.. contents::
19+
:local:
20+
21+
------------------------------------------------------------------------
22+
Variant: Concrete procedure(s)
23+
------------------------------------------------------------------------
24+
25+
.. admonition:: Syntax
26+
27+
``proc``
28+
29+
The ``proc`` tactic, when applied to concrete procedures, unfolds the
30+
procedure definition(s) at hand, replacing the procedure call(s)
31+
with the body(ies) of the corresponding procedure(s). The proof goal is
32+
then updated accordingly.
33+
34+
.. ecproof::
35+
:title: Hoare logic example
36+
37+
require import AllCore.
38+
39+
module M = {
40+
proc f(x : int) = {
41+
x <- x + 1;
42+
x <- x * 2;
43+
return x;
44+
}
45+
}.
46+
47+
pred p : int.
48+
pred q : int.
49+
50+
lemma L : hoare[M.f : p x ==> q res].
51+
proof.
52+
(*$*) proc.
53+
abort.
54+
55+
.. ecproof::
56+
:title: Probabilistic relational Hoare logic example
57+
58+
require import AllCore.
59+
60+
module M1 = {
61+
proc f(x : int) = {
62+
x <- x + 1;
63+
x <- x * 2;
64+
return x;
65+
}
66+
}.
67+
68+
module M2 = {
69+
proc f(x : int) = {
70+
x <- x * 10;
71+
x <- x - 3;
72+
return x;
73+
}
74+
}.
75+
76+
pred p : int & int.
77+
pred q : int & int.
78+
79+
lemma L : equiv[M1.f ~ M2.f : p x{1} x{2} ==> q res{1} res{2}].
80+
proof.
81+
(*$*) proc.
82+
abort.
83+
84+
------------------------------------------------------------------------
85+
Variant: Abstract procedure (non-relational)
86+
------------------------------------------------------------------------
87+
88+
.. admonition:: Syntax
89+
90+
``proc {formulaI}``
91+
92+
Here, ``{formulaI}`` is an invariant that should be preserved by the
93+
procedure. The invariant can refer to global variables not being modified
94+
by the procedure. To ensure that variables of interest cannot be modified,
95+
it may be necessary to add restrictions to the module type of the abstract procedure, specifying which globals are not accessed.
96+
97+
The tactic, when applied to abstract procedures, generates a proof
98+
obligation that the invariant holds initially (i.e., it is implied by the
99+
precondition) and another that the invariant is sufficient to ensure the
100+
postcondition. For every module argument to the abstract procedure, an
101+
additional proof obligation is generated to ensure that every procedure in
102+
the module argument preserves the invariant.
103+
104+
The probabilistic Hoare logic variant only works when the invariant is
105+
guaranteed to hold with probability 1. Therefore it requires the initial
106+
bound to be 1 and generates an additional proof obligation requiring that
107+
losslessness of procedures of the module arguments implies losslessness
108+
of the procedure under consideration.
109+
110+
.. ecproof::
111+
:title: Hoare logic example with abstract procedure
112+
113+
require import AllCore.
114+
115+
module type OT = {
116+
proc g1(): int
117+
proc g2(x: int): unit
118+
}.
119+
120+
module type MT (O: OT) = {
121+
proc f(x : int): int
122+
}.
123+
124+
module O = {
125+
var y: int
126+
proc g1() = {
127+
y <- y+1;
128+
return y;
129+
}
130+
131+
proc g2(x: int) = {
132+
}
133+
}.
134+
135+
pred p : int.
136+
pred q : int.
137+
pred inv : int.
138+
139+
lemma L (M <: MT {-O}): hoare[M(O).f : p x ==> q res].
140+
proof.
141+
(*$*) proc (inv O.y).
142+
- admit. (* Invariant holds initially *)
143+
- admit. (* Invariant implies postcondition *)
144+
- admit. (* Procedure g1 preserves invariant *)
145+
(* Procedure g2 preserves invariant *)
146+
abort.
147+
148+
.. ecproof::
149+
:title: Probabilistic Hoare logic example with abstract procedure
150+
151+
require import AllCore.
152+
153+
module type OT = {
154+
proc g1(): int
155+
proc g2(x: int): unit
156+
}.
157+
158+
module type MT (O: OT) = {
159+
proc f(x : int): int
160+
}.
161+
162+
module O = {
163+
var y: int
164+
proc g1() = {
165+
y <- y+1;
166+
return y;
167+
}
168+
169+
proc g2(x: int) = {
170+
}
171+
}.
172+
173+
174+
pred p : int.
175+
pred q : int.
176+
pred inv : int.
177+
178+
lemma L (M <: MT {-O}): phoare[M(O).f : p x ==> q res] = 1%r.
179+
proof.
180+
(*$*) proc (inv O.y).
181+
- admit. (* Invariant holds initially *)
182+
- admit. (* Invariant implies postcondition *)
183+
- admit. (* Losslessness of M(O).f *)
184+
- admit. (* Procedure g1 preserves invariant *)
185+
(* Procedure g2 preserves invariant *)
186+
abort.
187+
188+
.. ecproof::
189+
:title: Expectation Hoare logic example with abstract procedure
190+
191+
require import AllCore Xreal.
192+
193+
module type OT = {
194+
proc g1(): int
195+
proc g2(x: int): unit
196+
}.
197+
198+
module type MT (O: OT) = {
199+
proc f(x : int): int
200+
}.
201+
202+
module O = {
203+
var y: int
204+
proc g1() = {
205+
y <- y+1;
206+
return y;
207+
}
208+
209+
proc g2(x: int) = {
210+
}
211+
}.
212+
213+
214+
op p : int -> xreal.
215+
op q : int -> xreal.
216+
op inv : int -> xreal.
217+
218+
lemma L (M <: MT {-O}): ehoare[M(O).f : p x ==> q res].
219+
proof.
220+
(*$*) proc (inv O.y).
221+
- admit. (* Invariant holds initially *)
222+
- admit. (* Invariant implies postcondition *)
223+
- admit. (* Procedure g1 preserves invariant *)
224+
(* Procedure g2 preserves invariant *)
225+
abort.
226+
227+
228+
------------------------------------------------------------------------
229+
Variant: Abstract procedure (relational)
230+
------------------------------------------------------------------------
231+
232+
The relational variant of the ``proc`` tactic for abstract procedures
233+
requires both procedures to be the same, though their module arguments
234+
may differ.
235+
236+
.. admonition:: Syntax
237+
238+
- ``proc {formulaI}``
239+
- ``proc {formulaB} {formulaI}``
240+
- ``proc {formulaB} {formulaI} {formulaJ}``
241+
242+
Here:
243+
244+
- ``{formulaI}`` is a two-sided invariant that should be preserved by the
245+
pair of procedures.
246+
- ``{formulaB}`` is an optional formula representing a bad event on the
247+
right side after which the invariant need no longer hold.
248+
- ``{formulaJ}`` is an optional formula representing the invariant after
249+
the bad event has occurred. This is optional even if ``{formulaB}`` is
250+
provided; in which case the invariant is taken to be ``true`` after the
251+
bad event.
252+
253+
The tactic can be thought of as keeping both procedures in sync using
254+
``{formulaI}`` until the bad event ``{formulaB}`` occurs on the right
255+
side, after which they are no longer kept in sync. Instead ``{formulaJ}``
256+
is then preserved by the left and right procedures individually, no matter
257+
the order in which the two sides make progress.
258+
259+
When only ``{formulaI}`` is provided, the tactic works similarly to the
260+
non-relational variants, generating proof obligations to ensure that
261+
the invariant, equality of the globals of the module containing the
262+
procedure and equality of arguments holds and that equality of the
263+
globals, result and the invariant suffices to ensure the postcondition.
264+
For every procedure of every module argument to the abstract procedure
265+
an additional proof obligation is generated to ensure that the procedure
266+
pairs of the module arguments on the left and right preserve the invariant
267+
and yield equal results when called on equal arguments.
268+
269+
.. ecproof::
270+
:title: Simple Probabilistic Relational Hoare logic example
271+
272+
require import AllCore.
273+
274+
module type OT = {
275+
proc g1(): int
276+
proc g2(x: int): unit
277+
}.
278+
279+
module type MT (O: OT) = {
280+
proc f(x : int): int
281+
}.
282+
283+
module O1 = {
284+
var y: int
285+
proc g1() = {
286+
y <- y+1;
287+
return y;
288+
}
289+
290+
proc g2(x: int) = {
291+
}
292+
}.
293+
module O2 = {
294+
var y: int
295+
proc g1() = {
296+
return y;
297+
}
298+
299+
proc g2(x: int) = {
300+
y <- y-1;
301+
}
302+
}.
303+
304+
pred p : int & int.
305+
pred q : int & int.
306+
pred inv : int & int.
307+
308+
lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}].
309+
proof.
310+
(*$*) proc (inv O1.y{1} O2.y{2}).
311+
- admit. (* Invariant holds initially *)
312+
- admit. (* Invariant implies postcondition *)
313+
- admit. (* Procedure g1 preserves invariant *)
314+
(* Procedure g2 preserves invariant *)
315+
abort.
316+
317+
When ``{formulaB}`` and ``{formulaJ}`` are provided, the equality of
318+
arguments, results, globals and ``{formulaI}`` obligations are modified to
319+
only hold/need to hold conditional on the bad event not having occurred on
320+
the right side. When the bad event has occurred, we instead require that
321+
``{formulaJ}`` holds without any additional equality requirements. Since
322+
the behavior of the two sides is no longer synchronized after the bad
323+
event, an obligation is generated to ensure that the procedure is lossless
324+
when the procedures in its module arguments are lossless, to avoid the
325+
weights diverging after the bad event.
326+
327+
For every procedure of every module argument to the abstract procedure on
328+
the left, an additional proof obligation is generated to ensure that the
329+
when the bad event has happened and ``{formulaJ}`` holds for some right
330+
memory, then it is guaranteed to still hold for that right memory after
331+
running the procedure of the argument on the left. Similarly, for every
332+
procedure of every module argument to the abstract procedure on the right,
333+
an additional proof obligation is generated to ensure that when the bad
334+
event has happened and ``{formulaJ}`` holds for some left memory, then the
335+
bad event on the right and the two-sided invariant ``{formulaJ}`` is
336+
guaranteed to still hold for the left memory after running the procedure
337+
of the argument on the right.
338+
339+
If you want the bad event to be on the left side instead, you can swap the
340+
two programs using the ``sym`` tactic before applying ``proc``.
341+
342+
.. ecproof::
343+
:title: Probabilistic Relational Hoare logic example with bad event
344+
345+
require import AllCore.
346+
347+
module type OT = {
348+
proc g(): unit
349+
}.
350+
351+
module type MT (O: OT) = {
352+
proc f(x : int): int
353+
}.
354+
355+
module O1 = {
356+
var y: int
357+
proc g() = {
358+
y <- y+1;
359+
}
360+
}.
361+
module O2 = {
362+
var y: int
363+
proc g() = {
364+
y <- y-1;
365+
}
366+
}.
367+
368+
pred p : int & int.
369+
pred q : int & int.
370+
pred inv : int & int.
371+
pred bad : int.
372+
pred inv2 : int & int.
373+
374+
lemma L (M <: MT {-O1, -O2}): equiv[M(O1).f ~ M(O2).f: p x{1} x{2} ==> q res{1} res{2}].
375+
proof.
376+
(*$*) proc (bad O2.y) (inv O1.y{1} O2.y{2}) (inv2 O1.y{1} O2.y{2}).
377+
- admit. (* Connecting precondition to invariants *)
378+
- admit. (* Connecting invariants to postcondition *)
379+
- admit. (* Losslessness of M(O).f *)
380+
- admit. (* Relating O1.g and O2.g during synchronization *)
381+
- admit. (* Behaviour of O1.g after bad event *)
382+
(* Behaviour of O2.g after bad event *)
383+
abort.

‎refman/index.html‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -80,6 +80,7 @@ <h1>EasyCrypt reference manual<a class="headerlink" href="#easycrypt-reference-m
8080
<ul>
8181
<li class="toctree-l1"><a class="reference internal" href="tactics.html">Proof tactics reference</a><ul>
8282
<li class="toctree-l2"><a class="reference internal" href="tactics/if.html">Tactic: <code class="docutils literal notranslate"><span class="pre">if</span></code></a></li>
83+
<li class="toctree-l2"><a class="reference internal" href="tactics/proc.html">Tactic: <code class="docutils literal notranslate"><span class="pre">proc</span></code></a></li>
8384
<li class="toctree-l2"><a class="reference internal" href="tactics/skip.html">Tactic: <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">skip</span></code></a></li>
8485
<li class="toctree-l2"><a class="reference internal" href="tactics/splitwhile.html">Tactic: <code class="docutils literal notranslate"><span class="pre">splitwhile</span></code> Tactic</a></li>
8586
<li class="toctree-l2"><a class="reference internal" href="tactics/swap.html">Tactic: <code class="code highlight easycrypt docutils literal highlight-easycrypt"><span class="kr">swap</span></code></a></li>

‎refman/objects.inv‎

11 Bytes
Binary file not shown.

0 commit comments

Comments
 (0)