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.

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

Jump to bottom

Revive the Move prover #20339

Draft
wants to merge 126 commits into
base: main
Choose a base branch
from
Draft

Revive the Move prover #20339

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
126 commits
Select commit Hold shift + click to select a range
b864947
[experimental] bring back boogie generation pipeline
sblackshear Jul 28, 2024
5057f4a
Partial merge of aptos prover changes.
andreistefanescu Aug 16, 2024
6fd3d2f
Remove DenyList and dynamic_field dependency in coin.move.
andreistefanescu Jun 28, 2024
0e1d7d0
Add prover library
Aug 11, 2024
8563162
Update prover library
Aug 12, 2024
0bfffd0
Merge and improve aptos move prover changes for sui.
andreistefanescu Aug 27, 2024
7fa0fa0
Improve new spec language.
andreistefanescu Aug 30, 2024
4382508
Fix conflicting arguments in sui-move build
Sep 1, 2024
a39aca0
Export ids_created in tx_context.
andreistefanescu Sep 4, 2024
130d04c
Add fun_spec macro.
andreistefanescu Sep 5, 2024
a4675ed
Spec improvements.
andreistefanescu Sep 6, 2024
5ac004f
Add initial support for requires/ensures/aborts blocks, abort_if
Sep 9, 2024
851dd45
Add support for loop invariants.
andreistefanescu Sep 13, 2024
8e2794b
just comment identifying the invariant token, should become a regular…
cos Sep 14, 2024
b6d059f
and remove the offending spec
cos Sep 14, 2024
440605f
Check assert no-abort in loop invariants.
andreistefanescu Sep 16, 2024
c05dc2a
Refactor prover interface
Sep 17, 2024
d194aaf
Fix aborts boogie function generation.
andreistefanescu Sep 17, 2024
7b1ab73
Revert "Remove DenyList and dynamic_field dependency in coin.move."
andreistefanescu Sep 18, 2024
129e74f
Remove unused functions from boogie generation.
andreistefanescu Sep 18, 2024
377353b
Add support for prelude_extra.bpl.
andreistefanescu Sep 18, 2024
c463abd
Add invariant tests.
andreistefanescu Sep 18, 2024
008eb3c
Fix no-abort check in loop invariants.
andreistefanescu Sep 19, 2024
baf006d
wip opaque specs.
andreistefanescu Sep 25, 2024
4bd9790
wip opaque specs.
andreistefanescu Sep 26, 2024
45cb1cf
fresh
cos Sep 26, 2024
6e80dc6
Merge branch 'boogie_gen' of https://github.com/asymptotic-code/sui i…
cos Sep 26, 2024
64352cc
wip opaque specs.
andreistefanescu Sep 26, 2024
5759131
wip opaque specs.
andreistefanescu Sep 27, 2024
1f4bd8d
Fix integer to_u8/.../to_u256.
andreistefanescu Sep 27, 2024
800f0d6
wip opaque specs.
andreistefanescu Sep 27, 2024
dec114f
wip opaque specs.
andreistefanescu Sep 29, 2024
e93d15d
wip opaque specs.
andreistefanescu Sep 30, 2024
719675d
wip ghost variables.
andreistefanescu Oct 3, 2024
6fd60bd
wip
andreistefanescu Oct 3, 2024
39f2d92
wip
andreistefanescu Oct 7, 2024
c161247
Add some specs in sui-framework.
andreistefanescu Oct 7, 2024
f1c37e5
wip
andreistefanescu Oct 7, 2024
6106754
wip ghost variables declaration.
andreistefanescu Oct 8, 2024
315d91c
wip vector intrinsics.
andreistefanescu Oct 8, 2024
73bc60b
wip debug printout.
andreistefanescu Oct 8, 2024
d4ce6cf
noop specs
cos Oct 9, 2024
71f757f
wip print info
andreistefanescu Oct 9, 2024
08cbe04
wip ghost variables.
andreistefanescu Oct 9, 2024
da314e1
cargo fmt.
andreistefanescu Oct 9, 2024
cc932e6
wip
andreistefanescu Oct 9, 2024
249fffc
wip
andreistefanescu Oct 9, 2024
e924b67
wip
andreistefanescu Oct 11, 2024
7e685e1
wip
andreistefanescu Oct 11, 2024
ebc9788
Check well formedness for spec globals.
andreistefanescu Oct 11, 2024
680ae61
wip
andreistefanescu Oct 14, 2024
a10b1ac
wip
andreistefanescu Oct 15, 2024
ba5a468
wip
andreistefanescu Oct 16, 2024
652739f
wip
andreistefanescu Oct 17, 2024
3637c4b
use attributes.
andreistefanescu Oct 18, 2024
49597e2
Fix some unwrap panics.
andreistefanescu Oct 20, 2024
599ba5d
activate verify_only
cos Oct 21, 2024
0c95ecd
and filtering out invariant calls
cos Oct 21, 2024
7bd0e6d
wip
andreistefanescu Oct 21, 2024
46c1c5c
leave body in place
cos Oct 21, 2024
e8ef7e5
Merge branch 'specs5-temp' into boogie_gen
cos Oct 21, 2024
96b3114
fix
cos Oct 21, 2024
75ac380
fix
cos Oct 21, 2024
3b342f3
fixes
cos Oct 21, 2024
49b6a25
.
cos Oct 21, 2024
a93155f
tests passing
cos Oct 21, 2024
8e6c71e
wip
andreistefanescu Oct 22, 2024
fba7eee
wip
andreistefanescu Oct 22, 2024
96ec3c3
wip
andreistefanescu Oct 22, 2024
3104f39
Revert "leave body in place"
andreistefanescu Oct 23, 2024
fac02ac
prep wip.
andreistefanescu Oct 23, 2024
d2f41a0
prep wip.
andreistefanescu Oct 23, 2024
837a8d3
cleanup wip.
andreistefanescu Oct 23, 2024
f501244
add type invariants.
andreistefanescu Oct 24, 2024
0d38816
wip
andreistefanescu Oct 24, 2024
09c68c8
wip
andreistefanescu Oct 25, 2024
85f9748
fix loop invariants.
andreistefanescu Oct 25, 2024
b42d5d9
wip
andreistefanescu Oct 25, 2024
ed42ad1
wip
andreistefanescu Oct 25, 2024
6f72f81
wip
andreistefanescu Oct 25, 2024
c15b135
Merge branch 'main' of github.com:MystenLabs/sui into boogie_gen
andreistefanescu Nov 1, 2024
79a9284
wip verify_only.
andreistefanescu Nov 4, 2024
3214f8f
formatting.
andreistefanescu Nov 4, 2024
8650294
wip
andreistefanescu Nov 4, 2024
62d24e1
remove invariant and spec
cos Nov 5, 2024
a1c9843
remove extra
cos Nov 5, 2024
ffb4d85
add verify_only on use.
andreistefanescu Nov 5, 2024
e0fcb0c
wip
andreistefanescu Nov 8, 2024
9252cd3
wip amm.
andreistefanescu Nov 11, 2024
87deb5e
.
cos Nov 11, 2024
a24be05
Merge remote-tracking branch 'refs/remotes/origin/boogie_gen' into bo…
cos Nov 11, 2024
ac20ce7
fix tests
cos Nov 11, 2024
ed7695a
move test updates
cos Nov 11, 2024
2392d67
update spec deprecation tests
cos Nov 11, 2024
84162a2
specs
cos Nov 12, 2024
0fe6a17
add specs to test suite
cos Nov 12, 2024
e102904
map through Spanned
cos Nov 12, 2024
a619009
ast Exp_ traversal -- needs testing
cos Nov 12, 2024
efe20e7
remove warning
cos Nov 12, 2024
515fff9
wip on filtering
cos Nov 12, 2024
5ff3820
wip amm.
andreistefanescu Nov 14, 2024
bfa5ad5
wip
cos Nov 13, 2024
da2de8a
good
cos Nov 14, 2024
4785619
getting there
cos Nov 14, 2024
271f869
move and fix
cos Nov 14, 2024
465c321
fix
cos Nov 14, 2024
254c7c3
wip amm
andreistefanescu Nov 14, 2024
7021d88
wip amm.
andreistefanescu Nov 14, 2024
f942eed
wip
andreistefanescu Nov 14, 2024
f5f4093
wip amm.
andreistefanescu Nov 14, 2024
7a3f79d
rename verify_only to spec_only
cos Nov 14, 2024
0335721
focus
cos Nov 14, 2024
b90e25e
refactor
cos Nov 14, 2024
0f5bf92
.
cos Nov 14, 2024
d4a738a
wip
andreistefanescu Nov 15, 2024
6f084af
amm wip.
andreistefanescu Nov 15, 2024
7304df7
working
cos Nov 19, 2024
7ab83a0
wip
andreistefanescu Nov 19, 2024
81fe1f9
fix spec attribute.
andreistefanescu Nov 19, 2024
f416a84
remove amm
andreistefanescu Nov 19, 2024
7fb1dfa
boogie gen improvements.
andreistefanescu Nov 19, 2024
2eb67ad
_spec variables
cos Nov 19, 2024
667d94f
Merge remote-tracking branch 'sui/main' into revive_prover
cos Nov 20, 2024
76c340c
fixes.
andreistefanescu Nov 20, 2024
8ccbc13
cleanup.
andreistefanescu Nov 21, 2024
c25545a
remove old
cos Nov 21, 2024
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
243 changes: 235 additions & 8 deletions Cargo.lock
View file
Open in desktop

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

Loading
Loading