From 39be570a3bad7535b4fe44f9ac527ca59d00c2e9 Mon Sep 17 00:00:00 2001 From: seebees Date: Fri, 5 Nov 2021 20:52:27 -0700 Subject: [PATCH 1/2] fix: Add to gitignore --- .gitignore | 2 ++ 1 file changed, 2 insertions(+) diff --git a/.gitignore b/.gitignore index 806a7c87..3747e378 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,3 @@ **/Output/ +/.DS_Store +/.history From 51f59543458b88b9b00bcb199eee4a8501ec330e Mon Sep 17 00:00:00 2001 From: seebees Date: Fri, 5 Nov 2021 20:55:13 -0700 Subject: [PATCH 2/2] 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. --- src/Action.dfy | 32 +++ src/Action.dfy.expect | 2 + src/Collections/Sequences/Actions.dfy | 261 +++++++++++++++++++ src/Collections/Sequences/Actions.dfy.expect | 2 + 4 files changed, 297 insertions(+) create mode 100644 src/Action.dfy create mode 100644 src/Action.dfy.expect create mode 100644 src/Collections/Sequences/Actions.dfy create mode 100644 src/Collections/Sequences/Actions.dfy.expect diff --git a/src/Action.dfy b/src/Action.dfy new file mode 100644 index 00000000..32458bdf --- /dev/null +++ b/src/Action.dfy @@ -0,0 +1,32 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/******************************************************************************* +* Original: Copyright (c) 2020 Secure Foundations Lab +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +module Action { + + trait {:termination false} Action + { + method Invoke(a: A) + returns (r: R) + requires Requires(a) + ensures Ensures(a, r) + + predicate Requires(a: A) + predicate Ensures(a: A, r: R) + } + + trait {:termination false} NothingToRequire + { + predicate Requires(a: A){ + true + } + } + +} diff --git a/src/Action.dfy.expect b/src/Action.dfy.expect new file mode 100644 index 00000000..012f5b99 --- /dev/null +++ b/src/Action.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 0 verified, 0 errors diff --git a/src/Collections/Sequences/Actions.dfy b/src/Collections/Sequences/Actions.dfy new file mode 100644 index 00000000..3d795b61 --- /dev/null +++ b/src/Collections/Sequences/Actions.dfy @@ -0,0 +1,261 @@ +// RUN: %dafny /compile:0 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +/******************************************************************************* +* Original: Copyright (c) 2020 Secure Foundations Lab +* SPDX-License-Identifier: MIT +* +* Modifications and Extensions: Copyright by the contributors to the Dafny Project +* SPDX-License-Identifier: MIT +*******************************************************************************/ + +include "../../Wrappers.dfy" +include "../../Action.dfy" +include "Seq.dfy" + +module Actions { + import opened Wrappers + import opened A = Action + import opened Seq + + method Map( + action: Action, + s: seq + ) + returns (res: seq) + requires forall i | i in s :: action.Requires(i) + ensures |s| == |res| + ensures + forall i :: + && 0 <= i < |s| + ==> + action.Ensures(s[i], res[i]) + { + var rs := []; + for i := 0 to |s| + invariant |s[..i]| == |rs| + invariant forall j :: + && 0 <= j < i + ==> + action.Ensures(s[j], rs[j]) + { + var r := action.Invoke(s[i]); + rs := rs + [r]; + } + return rs; + } + + method MapWithResult( + action: Action>, + s: seq + ) + returns (res: Result, E>) + requires forall i | i in s :: action.Requires(i) + ensures + res.Success? + ==> + |s| == |res.value| + ensures + res.Success? + ==> + (forall i :: + && 0 <= i < |s| + ==> + action.Ensures(s[i], Success(res.value[i]))) + { + var rs := []; + for i := 0 to |s| + invariant |s[..i]| == |rs| + invariant forall j :: + && 0 <= j < i + ==> + action.Ensures(s[j], Success(rs[j])) + { + var maybeR := action.Invoke(s[i]); + if maybeR.Failure? { + return Failure(maybeR.error); + } + var r := maybeR.value; + rs := rs + [r]; + } + return Success(rs); + } + + method FlatMap( + action: Action>, + s: seq + ) + // The ghost parts is returned to facilitate + // threading proof obligations. + // Idealy, it would be great to remove this + // and simply prove everything about `res`. + // However in practice this has proven to be difficult. + // Given how flexible FlatMap is, + // there may not be a prcatical general solution. + returns (res: seq, ghost parts: seq>) + requires forall i | i in s :: action.Requires(i) + ensures + && |s| == |parts| + && res == Flatten(parts) + && (forall i :: 0 <= i < |s| + ==> + && action.Ensures(s[i], parts[i]) + && multiset(parts[i]) <= multiset(res)) + { + parts := []; + var rs := []; + for i := 0 to |s| + invariant |s[..i]| == |parts| + invariant forall j :: + && 0 <= j < i + ==> + && action.Ensures(s[j], parts[j]) + && multiset(parts[j]) <= multiset(rs) + invariant Flatten(parts) == rs + { + var r := action.Invoke(s[i]); + rs := rs + r; + LemmaFlattenConcat(parts, [r]); + parts := parts + [r]; + } + return rs, parts; + } + + method FlatMapWithResult( + action: Action, E>>, + s: seq + ) + // The ghost parts is returned to facilitate + // threading proof obligations. + // Idealy, it would be great to remove this + // and simply prove everything about `res`. + // However in practice this has proven to be difficult. + // Given how flexible FlatMap is, + // there may not be a prcatical general solution. + returns (res: Result, E>, ghost parts: seq>) + requires forall i | i in s :: action.Requires(i) + ensures + res.Success? + ==> + && |s| == |parts| + && res.value == Flatten(parts) + && (forall i :: 0 <= i < |s| + ==> + && action.Ensures(s[i], Success(parts[i])) + && multiset(parts[i]) <= multiset(res.value) + ) + { + parts := []; + var rs := []; + for i := 0 to |s| + invariant |s[..i]| == |parts| + invariant forall j :: + && 0 <= j < i + ==> + && action.Ensures(s[j], Success(parts[j])) + && multiset(parts[j]) <= multiset(rs) + invariant Flatten(parts) == rs + { + var maybeR := action.Invoke(s[i]); + if maybeR.Failure? { + return Failure(maybeR.error), parts; + } + var r := maybeR.value; + rs := rs + r; + LemmaFlattenConcat(parts, [r]); + parts := parts + [r]; + } + return Success(rs), parts; + } + + method Filter( + action: Action, + s: seq + ) + returns (res: seq) + requires forall i | i in s :: action.Requires(i) + ensures |s| >= |res| + ensures + forall j :: + j in res + ==> + && j in s + && action.Ensures(j, true) + { + var rs := []; + for i := 0 to |s| + invariant |s[..i]| >= |rs| + invariant forall j :: + j in rs + ==> + && j in s + && action.Ensures(j, true) + { + var r := action.Invoke(s[i]); + if r { + rs := rs + [s[i]]; + } + } + return rs; + } + + method FilterWithResult( + action: Action>, + s: seq + ) + returns (res: Result, E>) + requires forall i | i in s :: action.Requires(i) + ensures + res.Success? + ==> + && |s| >= |res.value| + && forall j :: + j in res.value + ==> + && j in s + && action.Ensures(j, Success(true)) + { + var rs := []; + for i := 0 to |s| + invariant |s[..i]| >= |rs| + invariant forall j :: + j in rs + ==> + && j in s + && action.Ensures(j, Success(true)) + { + var maybeR := action.Invoke(s[i]); + if maybeR.Failure? { + return Failure(maybeR.error); + } + var r := maybeR.value; + if r { + rs := rs + [s[i]]; + } + } + return Success(rs); + } + + method ReduceToSuccess( + action: Action>, + s: seq + ) + returns (res: Result>) + requires forall i | i in s :: action.Requires(i) + ensures + res.Success? + ==> + exists a | a in s :: action.Ensures(a, Success(res.value)) + { + var errors := []; + for i := 0 to |s| { + var attempt := action.Invoke(s[i]); + if attempt.Success? { + return Success(attempt.value); + } else { + errors := errors + [attempt.error]; + } + } + return Failure(errors); + } +} diff --git a/src/Collections/Sequences/Actions.dfy.expect b/src/Collections/Sequences/Actions.dfy.expect new file mode 100644 index 00000000..f28a89f4 --- /dev/null +++ b/src/Collections/Sequences/Actions.dfy.expect @@ -0,0 +1,2 @@ + +Dafny program verifier finished with 88 verified, 0 errors