Skip to content
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.

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

Fix: Opaque functions guaranteed to be opaque until revealed #3779

Merged
merged 33 commits into from
Apr 21, 2023
Merged
Changes from 1 commit
Commits
Show all changes
33 commits
Select commit Hold shift + click to select a range
91c3cba
Add test for issue #3719
MikaelMayer Mar 20, 2023
f8c7c2a
Fix: Opaque functions guaranteed to be opaque until revealed
MikaelMayer Mar 21, 2023
83653e4
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 22, 2023
317cd20
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 27, 2023
f681d8c
FIXER:dafny0/DafnyLibClient.dfy
MikaelMayer Mar 27, 2023
a6b8e06
Ensured no key is missing
MikaelMayer Mar 27, 2023
ac43ca0
FIXER:vstte2012/BreadthFirstSearch.dfy
MikaelMayer Mar 28, 2023
bea41bb
Ensure that CanRevealFuel is compatible with AsFuelBottom
MikaelMayer Mar 28, 2023
f87936b
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 28, 2023
efb05bd
FIXER:VSI-Benchmarks/b4.dfy
MikaelMayer Mar 28, 2023
af7d56e
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 29, 2023
2e50c64
Merge branch 'fix-3719-opaque-leaked-lambda' of https://github.com/da…
MikaelMayer Mar 30, 2023
1db3d5a
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 30, 2023
dfad0e1
Improved proof durability of vstte2012/BreadthFirstSearch.dfy
MikaelMayer Mar 31, 2023
faf586d
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 31, 2023
e86f57a
Update BreadthFirstSearch.dfy
MikaelMayer Mar 31, 2023
949b62b
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Mar 31, 2023
05a3ed7
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 3, 2023
b813dba
Review comments
MikaelMayer Apr 4, 2023
330c504
Merge branch 'fix-3719-opaque-leaked-lambda' of https://github.com/da…
MikaelMayer Apr 4, 2023
d989bf5
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 4, 2023
6a82ed6
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 5, 2023
9030011
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 6, 2023
a2061ab
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 7, 2023
107a31d
FIXER:dafny4/ACL2-extractor.dfy
MikaelMayer Apr 7, 2023
ae261d1
fixed CI
MikaelMayer Apr 10, 2023
cf3eb94
Clever use of split_here to avoid resource limit on bfs
MikaelMayer Apr 10, 2023
a7c8653
Fixed CI
MikaelMayer Apr 17, 2023
9289b3b
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 17, 2023
a32bdaa
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 17, 2023
68ba07b
Merge branch 'master' into fix-3719-opaque-leaked-lambda
MikaelMayer Apr 18, 2023
3f12326
Merge branch 'master' into fix-3719-opaque-leaked-lambda
atomb Apr 20, 2023
985eabf
Update msbuild.yml
MikaelMayer Apr 21, 2023
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
10 changes: 7 additions & 3 deletions Test/vstte2012/BreadthFirstSearch.dfy
Original file line number Diff line number Diff line change
@@ -26,7 +26,7 @@ class BreadthFirstSearch<Vertex(==)>
// this method returns, as a ghost out-parameter, that existential
// witness. The method could equally well have been written using an
// existential quantifier and no ghost out-parameter.
method {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set<Vertex>)
method {:rlimit 5000} {:vcs_split_on_every_assert} BFS(source: Vertex, dest: Vertex, ghost AllVertices: set<Vertex>)
returns (d: int, ghost path: List<Vertex>)
// source and dest are among AllVertices
requires source in AllVertices && dest in AllVertices;
@@ -86,9 +86,10 @@ class BreadthFirstSearch<Vertex(==)>
{
// remove a vertex "v" from "C"
var v :| v in C;
assert v != dest && C == {v} ==>
(Processed + {v}) + (N + (set w | w in Succ(v) && w !in V)) == R(source, d+1, AllVertices) by { reveal R(); }
C, Processed := C - {v}, Processed + {v};
ghost var pathToV := Find(source, v, paths);

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is there a reason to remove these blank lines?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No indeed that does not improve verifiability :-)

if v == dest {
forall p | IsPath(source, dest, p)
ensures length(pathToV) <= length(p);
@@ -98,13 +99,16 @@ class BreadthFirstSearch<Vertex(==)>
if length(p) < length(pathToV) {
// show that this branch is impossible
RMonotonicity(source, length(p), d-1, AllVertices);
assert false;
}
}
return d, pathToV;
}

// process newly encountered successors
var newlyEncountered := set w | w in Succ(v) && w !in V;
assert if C == {} then
Processed + (N + newlyEncountered) == R(source, d+1, AllVertices)
else Processed + C == R(source, d, AllVertices) by { reveal R(); }
V, N := V + newlyEncountered, N + newlyEncountered;
paths := UpdatePaths(newlyEncountered, source, paths, v, pathToV);