Skip to content

Commit 51f5954

Browse files
seebeesseebees
committed
feat: Functional constructs for methods
Being able to express logic with map and filter simplifies the expression of an implementation. However doing this iteration in a method requires a loop. Loop invariants are hard.
1 parent 39be570 commit 51f5954

File tree

4 files changed

+297
-0
lines changed

4 files changed

+297
-0
lines changed

‎src/Action.dfy‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
// RUN: %dafny /compile:0 "%s" > "%t"
2+
// RUN: %diff "%s.expect" "%t"
3+
4+
/*******************************************************************************
5+
* Original: Copyright (c) 2020 Secure Foundations Lab
6+
* SPDX-License-Identifier: MIT
7+
*
8+
* Modifications and Extensions: Copyright by the contributors to the Dafny Project
9+
* SPDX-License-Identifier: MIT
10+
*******************************************************************************/
11+
12+
module Action {
13+
14+
trait {:termination false} Action<A, R>
15+
{
16+
method Invoke(a: A)
17+
returns (r: R)
18+
requires Requires(a)
19+
ensures Ensures(a, r)
20+
21+
predicate Requires(a: A)
22+
predicate Ensures(a: A, r: R)
23+
}
24+
25+
trait {:termination false} NothingToRequire<A>
26+
{
27+
predicate Requires(a: A){
28+
true
29+
}
30+
}
31+
32+
}

‎src/Action.dfy.expect‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
2+
Dafny program verifier finished with 0 verified, 0 errors

‎src/Collections/Sequences/Actions.dfy‎

Lines changed: 261 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,261 @@
1+
// RUN: %dafny /compile:0 "%s" > "%t"
2+
// RUN: %diff "%s.expect" "%t"
3+
4+
/*******************************************************************************
5+
* Original: Copyright (c) 2020 Secure Foundations Lab
6+
* SPDX-License-Identifier: MIT
7+
*
8+
* Modifications and Extensions: Copyright by the contributors to the Dafny Project
9+
* SPDX-License-Identifier: MIT
10+
*******************************************************************************/
11+
12+
include "../../Wrappers.dfy"
13+
include "../../Action.dfy"
14+
include "Seq.dfy"
15+
16+
module Actions {
17+
import opened Wrappers
18+
import opened A = Action
19+
import opened Seq
20+
21+
method Map<A, R>(
22+
action: Action<A, R>,
23+
s: seq<A>
24+
)
25+
returns (res: seq<R>)
26+
requires forall i | i in s :: action.Requires(i)
27+
ensures |s| == |res|
28+
ensures
29+
forall i ::
30+
&& 0 <= i < |s|
31+
==>
32+
action.Ensures(s[i], res[i])
33+
{
34+
var rs := [];
35+
for i := 0 to |s|
36+
invariant |s[..i]| == |rs|
37+
invariant forall j ::
38+
&& 0 <= j < i
39+
==>
40+
action.Ensures(s[j], rs[j])
41+
{
42+
var r := action.Invoke(s[i]);
43+
rs := rs + [r];
44+
}
45+
return rs;
46+
}
47+
48+
method MapWithResult<A, R, E>(
49+
action: Action<A, Result<R, E>>,
50+
s: seq<A>
51+
)
52+
returns (res: Result<seq<R>, E>)
53+
requires forall i | i in s :: action.Requires(i)
54+
ensures
55+
res.Success?
56+
==>
57+
|s| == |res.value|
58+
ensures
59+
res.Success?
60+
==>
61+
(forall i ::
62+
&& 0 <= i < |s|
63+
==>
64+
action.Ensures(s[i], Success(res.value[i])))
65+
{
66+
var rs := [];
67+
for i := 0 to |s|
68+
invariant |s[..i]| == |rs|
69+
invariant forall j ::
70+
&& 0 <= j < i
71+
==>
72+
action.Ensures(s[j], Success(rs[j]))
73+
{
74+
var maybeR := action.Invoke(s[i]);
75+
if maybeR.Failure? {
76+
return Failure(maybeR.error);
77+
}
78+
var r := maybeR.value;
79+
rs := rs + [r];
80+
}
81+
return Success(rs);
82+
}
83+
84+
method FlatMap<A, R>(
85+
action: Action<A, seq<R>>,
86+
s: seq<A>
87+
)
88+
// The ghost parts is returned to facilitate
89+
// threading proof obligations.
90+
// Idealy, it would be great to remove this
91+
// and simply prove everything about `res`.
92+
// However in practice this has proven to be difficult.
93+
// Given how flexible FlatMap is,
94+
// there may not be a prcatical general solution.
95+
returns (res: seq<R>, ghost parts: seq<seq<R>>)
96+
requires forall i | i in s :: action.Requires(i)
97+
ensures
98+
&& |s| == |parts|
99+
&& res == Flatten(parts)
100+
&& (forall i :: 0 <= i < |s|
101+
==>
102+
&& action.Ensures(s[i], parts[i])
103+
&& multiset(parts[i]) <= multiset(res))
104+
{
105+
parts := [];
106+
var rs := [];
107+
for i := 0 to |s|
108+
invariant |s[..i]| == |parts|
109+
invariant forall j ::
110+
&& 0 <= j < i
111+
==>
112+
&& action.Ensures(s[j], parts[j])
113+
&& multiset(parts[j]) <= multiset(rs)
114+
invariant Flatten(parts) == rs
115+
{
116+
var r := action.Invoke(s[i]);
117+
rs := rs + r;
118+
LemmaFlattenConcat(parts, [r]);
119+
parts := parts + [r];
120+
}
121+
return rs, parts;
122+
}
123+
124+
method FlatMapWithResult<A, R, E>(
125+
action: Action<A, Result<seq<R>, E>>,
126+
s: seq<A>
127+
)
128+
// The ghost parts is returned to facilitate
129+
// threading proof obligations.
130+
// Idealy, it would be great to remove this
131+
// and simply prove everything about `res`.
132+
// However in practice this has proven to be difficult.
133+
// Given how flexible FlatMap is,
134+
// there may not be a prcatical general solution.
135+
returns (res: Result<seq<R>, E>, ghost parts: seq<seq<R>>)
136+
requires forall i | i in s :: action.Requires(i)
137+
ensures
138+
res.Success?
139+
==>
140+
&& |s| == |parts|
141+
&& res.value == Flatten(parts)
142+
&& (forall i :: 0 <= i < |s|
143+
==>
144+
&& action.Ensures(s[i], Success(parts[i]))
145+
&& multiset(parts[i]) <= multiset(res.value)
146+
)
147+
{
148+
parts := [];
149+
var rs := [];
150+
for i := 0 to |s|
151+
invariant |s[..i]| == |parts|
152+
invariant forall j ::
153+
&& 0 <= j < i
154+
==>
155+
&& action.Ensures(s[j], Success(parts[j]))
156+
&& multiset(parts[j]) <= multiset(rs)
157+
invariant Flatten(parts) == rs
158+
{
159+
var maybeR := action.Invoke(s[i]);
160+
if maybeR.Failure? {
161+
return Failure(maybeR.error), parts;
162+
}
163+
var r := maybeR.value;
164+
rs := rs + r;
165+
LemmaFlattenConcat(parts, [r]);
166+
parts := parts + [r];
167+
}
168+
return Success(rs), parts;
169+
}
170+
171+
method Filter<A>(
172+
action: Action<A, bool>,
173+
s: seq<A>
174+
)
175+
returns (res: seq<A>)
176+
requires forall i | i in s :: action.Requires(i)
177+
ensures |s| >= |res|
178+
ensures
179+
forall j ::
180+
j in res
181+
==>
182+
&& j in s
183+
&& action.Ensures(j, true)
184+
{
185+
var rs := [];
186+
for i := 0 to |s|
187+
invariant |s[..i]| >= |rs|
188+
invariant forall j ::
189+
j in rs
190+
==>
191+
&& j in s
192+
&& action.Ensures(j, true)
193+
{
194+
var r := action.Invoke(s[i]);
195+
if r {
196+
rs := rs + [s[i]];
197+
}
198+
}
199+
return rs;
200+
}
201+
202+
method FilterWithResult<A, E>(
203+
action: Action<A, Result<bool, E>>,
204+
s: seq<A>
205+
)
206+
returns (res: Result<seq<A>, E>)
207+
requires forall i | i in s :: action.Requires(i)
208+
ensures
209+
res.Success?
210+
==>
211+
&& |s| >= |res.value|
212+
&& forall j ::
213+
j in res.value
214+
==>
215+
&& j in s
216+
&& action.Ensures(j, Success(true))
217+
{
218+
var rs := [];
219+
for i := 0 to |s|
220+
invariant |s[..i]| >= |rs|
221+
invariant forall j ::
222+
j in rs
223+
==>
224+
&& j in s
225+
&& action.Ensures(j, Success(true))
226+
{
227+
var maybeR := action.Invoke(s[i]);
228+
if maybeR.Failure? {
229+
return Failure(maybeR.error);
230+
}
231+
var r := maybeR.value;
232+
if r {
233+
rs := rs + [s[i]];
234+
}
235+
}
236+
return Success(rs);
237+
}
238+
239+
method ReduceToSuccess<A, B, E>(
240+
action: Action<A, Result<B, E>>,
241+
s: seq<A>
242+
)
243+
returns (res: Result<B, seq<E>>)
244+
requires forall i | i in s :: action.Requires(i)
245+
ensures
246+
res.Success?
247+
==>
248+
exists a | a in s :: action.Ensures(a, Success(res.value))
249+
{
250+
var errors := [];
251+
for i := 0 to |s| {
252+
var attempt := action.Invoke(s[i]);
253+
if attempt.Success? {
254+
return Success(attempt.value);
255+
} else {
256+
errors := errors + [attempt.error];
257+
}
258+
}
259+
return Failure(errors);
260+
}
261+
}

‎src/Collections/Sequences/Actions.dfy.expect‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
2+
Dafny program verifier finished with 88 verified, 0 errors

0 commit comments

Comments
 (0)