Code

Revive the Move prover#20339

Code

Draft

cos wants to merge 137 commits intoMystenLabs:mainMystenLabs/sui:mainfrom asymptotic-code:revive_proverasymptotic-code/sui:revive_proverCopy head branch name to clipboard

+31,081-1,593

Commits

Commits on Aug 14, 2024

• [experimental] bring back boogie generation pipeline

  sblackshear

  committed
  b864947

  Copy full SHA for b864947

Commits on Aug 17, 2024

• Partial merge of aptos prover changes.

  andreistefanescu

  committed
  5057f4a

  Copy full SHA for 5057f4a

Commits on Aug 29, 2024

• Remove DenyList and dynamic_field dependency in coin.move.

  andreistefanescu

  committed
  6fd3d2f

  Copy full SHA for 6fd3d2f

• Add prover library

  

  sam

  authored and

  andreistefanescu

  committed
  0e1d7d0

  Copy full SHA for 0e1d7d0

• Update prover library

  

  sam

  authored and

  andreistefanescu

  committed
  8563162

  Copy full SHA for 8563162

• Merge and improve aptos move prover changes for sui.

  andreistefanescu

  committed
  0bfffd0

  Copy full SHA for 0bfffd0

Commits on Aug 31, 2024

• Improve new spec language.

  andreistefanescu

  committed
  7fa0fa0

  Copy full SHA for 7fa0fa0

Commits on Sep 1, 2024

• Fix conflicting arguments in sui-move build

  

  sam

  committed
  4382508

  Copy full SHA for 4382508

Commits on Sep 5, 2024

• Export ids_created in tx_context.

  andreistefanescu

  committed
  a39aca0

  Copy full SHA for a39aca0

• Add fun_spec macro.

  andreistefanescu

  committed
  130d04c

  Copy full SHA for 130d04c

Commits on Sep 6, 2024

• Spec improvements.

  andreistefanescu

  committed
  a4675ed

  Copy full SHA for a4675ed

Commits on Sep 9, 2024

• Add initial support for requires/ensures/aborts blocks, abort_if

  

  sam

  committed
  5ac004f

  Copy full SHA for 5ac004f

Commits on Sep 13, 2024

• Add support for loop invariants.

  andreistefanescu

  committed
  851dd45

  Copy full SHA for 851dd45

Commits on Sep 14, 2024

• just comment identifying the invariant token, should become a regular identifier now

  cos

  committed
  8e2794b

  Copy full SHA for 8e2794b

• and remove the offending spec

  cos

  committed
  b6d059f

  Copy full SHA for b6d059f

Commits on Sep 16, 2024

• Check assert no-abort in loop invariants.

  andreistefanescu

  committed
  440605f

  Copy full SHA for 440605f

Commits on Sep 17, 2024

• Refactor prover interface

  

  sam

  committed
  c05dc2a

  Copy full SHA for c05dc2a

• Fix aborts boogie function generation.

  andreistefanescu

  committed
  d194aaf

  Copy full SHA for d194aaf

Commits on Sep 18, 2024

• Revert "Remove DenyList and dynamic_field dependency in coin.move."

  Show description for 7b1ab73
  andreistefanescu

  committed
  7b1ab73

  Copy full SHA for 7b1ab73

• Remove unused functions from boogie generation.

  andreistefanescu

  committed
  129e74f

  Copy full SHA for 129e74f

• Add support for prelude_extra.bpl.

  andreistefanescu

  committed
  377353b

  Copy full SHA for 377353b

• Add invariant tests.

  andreistefanescu

  committed
  c463abd

  Copy full SHA for c463abd

Commits on Sep 19, 2024

• Fix no-abort check in loop invariants.

  andreistefanescu

  committed
  008eb3c

  Copy full SHA for 008eb3c

Commits on Sep 25, 2024

• wip opaque specs.

  andreistefanescu

  committed
  baf006d

  Copy full SHA for baf006d

Commits on Sep 26, 2024

• wip opaque specs.

  andreistefanescu

  committed
  4bd9790

  Copy full SHA for 4bd9790

• fresh

  cos

  committed
  45cb1cf

  Copy full SHA for 45cb1cf

• Merge branch 'boogie_gen' of https://github.com/asymptotic-code/sui into boogie_gen

  cos

  committed
  6e80dc6

  Copy full SHA for 6e80dc6

• wip opaque specs.

  andreistefanescu

  committed
  64352cc

  Copy full SHA for 64352cc

Commits on Sep 27, 2024

• wip opaque specs.

  andreistefanescu

  committed
  5759131

  Copy full SHA for 5759131

• Fix integer to_u8/.../to_u256.

  andreistefanescu

  committed
  1f4bd8d

  Copy full SHA for 1f4bd8d

• wip opaque specs.

  andreistefanescu

  committed
  800f0d6

  Copy full SHA for 800f0d6

Commits on Sep 29, 2024

• wip opaque specs.

  andreistefanescu

  committed
  dec114f

  Copy full SHA for dec114f

Commits on Sep 30, 2024

• wip opaque specs.

  andreistefanescu

  committed
  e93d15d

  Copy full SHA for e93d15d

Commits on Oct 3, 2024

• wip ghost variables.

  andreistefanescu

  committed
  719675d

  Copy full SHA for 719675d

• wip

  andreistefanescu

  committed
  6fd60bd

  Copy full SHA for 6fd60bd

Commits on Oct 7, 2024

• wip

  andreistefanescu

  committed
  39f2d92

  Copy full SHA for 39f2d92

• Add some specs in sui-framework.

  andreistefanescu

  committed
  c161247

  Copy full SHA for c161247

• wip

  andreistefanescu

  committed
  f1c37e5

  Copy full SHA for f1c37e5

Commits on Oct 8, 2024

• wip ghost variables declaration.

  andreistefanescu

  committed
  6106754

  Copy full SHA for 6106754

• wip vector intrinsics.

  andreistefanescu

  committed
  315d91c

  Copy full SHA for 315d91c

• wip debug printout.

  andreistefanescu

  committed
  73bc60b

  Copy full SHA for 73bc60b

Commits on Oct 9, 2024

• noop specs

  cos

  committed
  d4ce6cf

  Copy full SHA for d4ce6cf

• wip print info

  andreistefanescu

  committed
  71f757f

  Copy full SHA for 71f757f

• wip ghost variables.

  andreistefanescu

  committed
  08cbe04

  Copy full SHA for 08cbe04

• cargo fmt.

  andreistefanescu

  committed
  da314e1

  Copy full SHA for da314e1

• wip

  andreistefanescu

  committed
  cc932e6

  Copy full SHA for cc932e6

• wip

  andreistefanescu

  committed
  249fffc

  Copy full SHA for 249fffc

Commits on Oct 11, 2024

• wip

  andreistefanescu

  committed
  e924b67

  Copy full SHA for e924b67

• wip

  andreistefanescu

  committed
  7e685e1

  Copy full SHA for 7e685e1

• Check well formedness for spec globals.

  andreistefanescu

  committed
  ebc9788

  Copy full SHA for ebc9788

Commits on Oct 15, 2024

• wip

  andreistefanescu

  committed
  680ae61

  Copy full SHA for 680ae61

• wip

  andreistefanescu

  committed
  a10b1ac

  Copy full SHA for a10b1ac

Commits on Oct 16, 2024

• wip

  andreistefanescu

  committed
  ba5a468

  Copy full SHA for ba5a468

Commits on Oct 17, 2024

• wip

  andreistefanescu

  committed
  652739f

  Copy full SHA for 652739f

Commits on Oct 18, 2024

• use attributes.

  andreistefanescu

  committed
  3637c4b

  Copy full SHA for 3637c4b

Commits on Oct 20, 2024

• Fix some unwrap panics.

  andreistefanescu

  committed
  49597e2

  Copy full SHA for 49597e2

Commits on Oct 21, 2024

• activate verify_only

  cos

  committed
  599ba5d

  Copy full SHA for 599ba5d

• and filtering out invariant calls

  cos

  committed
  0c95ecd

  Copy full SHA for 0c95ecd

• wip

  andreistefanescu

  committed
  7bd0e6d

  Copy full SHA for 7bd0e6d

• leave body in place

  cos

  committed
  46c1c5c

  Copy full SHA for 46c1c5c

• Merge branch 'specs5-temp' into boogie_gen

  cos

  committed
  e8ef7e5

  Copy full SHA for e8ef7e5

• fix

  cos

  committed
  96b3114

  Copy full SHA for 96b3114

• fix

  cos

  committed
  75ac380

  Copy full SHA for 75ac380

• fixes

  cos

  committed
  3b342f3

  Copy full SHA for 3b342f3

• .

  cos

  committed
  49b6a25

  Copy full SHA for 49b6a25

• tests passing

  cos

  committed
  a93155f

  Copy full SHA for a93155f

Commits on Oct 22, 2024

• wip

  andreistefanescu

  committed
  8e6c71e

  Copy full SHA for 8e6c71e

• wip

  andreistefanescu

  committed
  fba7eee

  Copy full SHA for fba7eee

• wip

  andreistefanescu

  committed
  96ec3c3

  Copy full SHA for 96ec3c3

Commits on Oct 23, 2024

• Revert "leave body in place"

  Show description for 3104f39
  andreistefanescu

  committed
  3104f39

  Copy full SHA for 3104f39

• prep wip.

  andreistefanescu

  committed
  fac02ac

  Copy full SHA for fac02ac

• prep wip.

  andreistefanescu

  committed
  d2f41a0

  Copy full SHA for d2f41a0

• cleanup wip.

  andreistefanescu

  committed
  837a8d3

  Copy full SHA for 837a8d3

Commits on Oct 24, 2024

• add type invariants.

  andreistefanescu

  committed
  f501244

  Copy full SHA for f501244

• wip

  andreistefanescu

  committed
  0d38816

  Copy full SHA for 0d38816

Commits on Oct 25, 2024

• wip

  andreistefanescu

  committed
  09c68c8

  Copy full SHA for 09c68c8

• fix loop invariants.

  andreistefanescu

  committed
  85f9748

  Copy full SHA for 85f9748

• wip

  andreistefanescu

  committed
  b42d5d9

  Copy full SHA for b42d5d9

• wip

  andreistefanescu

  committed
  ed42ad1

  Copy full SHA for ed42ad1

• wip

  andreistefanescu

  committed
  6f72f81

  Copy full SHA for 6f72f81

Commits on Nov 1, 2024

• Merge branch 'main' of github.com:MystenLabs/sui into boogie_gen

  andreistefanescu

  committed
  c15b135

  Copy full SHA for c15b135

Commits on Nov 4, 2024

• wip verify_only.

  andreistefanescu

  committed
  79a9284

  Copy full SHA for 79a9284

• formatting.

  andreistefanescu

  committed
  3214f8f

  Copy full SHA for 3214f8f

• wip

  andreistefanescu

  committed
  8650294

  Copy full SHA for 8650294

Commits on Nov 5, 2024

• remove invariant and spec

  cos

  committed
  62d24e1

  Copy full SHA for 62d24e1

• remove extra

  cos

  committed
  a1c9843

  Copy full SHA for a1c9843

• add verify_only on use.

  andreistefanescu

  committed
  ffb4d85

  Copy full SHA for ffb4d85

Commits on Nov 8, 2024

• wip

  andreistefanescu

  committed
  e0fcb0c

  Copy full SHA for e0fcb0c

Commits on Nov 11, 2024

• wip amm.

  andreistefanescu

  committed
  9252cd3

  Copy full SHA for 9252cd3

• .

  cos

  committed
  87deb5e

  Copy full SHA for 87deb5e

• Merge remote-tracking branch 'refs/remotes/origin/boogie_gen' into boogie_gen

  cos

  committed
  a24be05

  Copy full SHA for a24be05

• fix tests

  cos

  committed
  ac20ce7

  Copy full SHA for ac20ce7

• move test updates

  cos

  committed
  ed7695a

  Copy full SHA for ed7695a

• update spec deprecation tests

  cos

  committed
  2392d67

  Copy full SHA for 2392d67

Commits on Nov 12, 2024

• specs

  cos

  committed
  84162a2

  Copy full SHA for 84162a2

• add specs to test suite

  cos

  committed
  0fe6a17

  Copy full SHA for 0fe6a17

• map through Spanned

  cos

  committed
  e102904

  Copy full SHA for e102904

• ast Exp_ traversal -- needs testing

  cos

  committed
  a619009

  Copy full SHA for a619009

• remove warning

  cos

  committed
  efe20e7

  Copy full SHA for efe20e7

• wip on filtering

  cos

  committed
  515fff9

  Copy full SHA for 515fff9

Commits on Nov 14, 2024

• wip amm.

  andreistefanescu

  committed
  5ff3820

  Copy full SHA for 5ff3820

• wip

  cos

  committed
  bfa5ad5

  Copy full SHA for bfa5ad5

• good

  cos

  committed
  da2de8a

  Copy full SHA for da2de8a

• getting there

  cos

  committed
  4785619

  Copy full SHA for 4785619

• move and fix

  cos

  committed
  271f869

  Copy full SHA for 271f869

• fix

  cos

  committed
  465c321

  Copy full SHA for 465c321

• wip amm

  andreistefanescu

  committed
  254c7c3

  Copy full SHA for 254c7c3

• wip amm.

  andreistefanescu

  committed
  7021d88

  Copy full SHA for 7021d88

• wip

  andreistefanescu

  committed
  f942eed

  Copy full SHA for f942eed

• wip amm.

  andreistefanescu

  committed
  f5f4093

  Copy full SHA for f5f4093

• rename verify_only to spec_only

  cos

  committed
  7a3f79d

  Copy full SHA for 7a3f79d

• focus

  cos

  committed
  0335721

  Copy full SHA for 0335721

• refactor

  cos

  committed
  b90e25e

  Copy full SHA for b90e25e

• .

  cos

  committed
  0f5bf92

  Copy full SHA for 0f5bf92

Commits on Nov 15, 2024

• wip

  andreistefanescu

  committed
  d4a738a

  Copy full SHA for d4a738a

• amm wip.

  andreistefanescu

  committed
  6f084af

  Copy full SHA for 6f084af

Commits on Nov 19, 2024

• working

  cos

  committed
  7304df7

  Copy full SHA for 7304df7

• wip

  andreistefanescu

  committed
  7ab83a0

  Copy full SHA for 7ab83a0

• fix spec attribute.

  andreistefanescu

  committed
  81fe1f9

  Copy full SHA for 81fe1f9

• remove amm

  andreistefanescu

  committed
  f416a84

  Copy full SHA for f416a84

• boogie gen improvements.

  andreistefanescu

  committed
  7fb1dfa

  Copy full SHA for 7fb1dfa

• _spec variables

  cos

  committed
  2eb67ad

  Copy full SHA for 2eb67ad

Commits on Nov 20, 2024

• Merge remote-tracking branch 'sui/main' into revive_prover

  cos

  committed
  667d94f

  Copy full SHA for 667d94f

• fixes.

  andreistefanescu

  committed
  76c340c

  Copy full SHA for 76c340c

Commits on Nov 21, 2024

• cleanup.

  andreistefanescu

  committed
  8ccbc13

  Copy full SHA for 8ccbc13

• remove old

  cos

  committed
  c25545a

  Copy full SHA for c25545a

Commits on Dec 18, 2024

• fix.

  andreistefanescu

  committed
  6bba483

  Copy full SHA for 6bba483

Commits on Jan 6, 2025

• docs: wip on guide

  cos

  committed
  2fc122e

  Copy full SHA for 2fc122e

• .

  cos

  committed
  29ab37b

  Copy full SHA for 29ab37b

• docs: prover reference wip

  cos

  committed
  b1eed71

  Copy full SHA for b1eed71

• .

  cos

  committed
  81da6db

  Copy full SHA for 81da6db

Commits on Jan 10, 2025

• complete reference

  cos

  committed
  28bb348

  Copy full SHA for 28bb348

• integrate Andrei's feedback

  cos

  committed
  e31e600

  Copy full SHA for e31e600

• .

  cos

  committed
  fb42174

  Copy full SHA for fb42174

Commits on Jan 11, 2025

• update docs, and add fix

  cos

  committed
  a42be27

  Copy full SHA for a42be27

Commits on Jan 13, 2025

• integrate Andrei's feedback

  cos

  committed
  5d49a48

  Copy full SHA for 5d49a48

Commits on Jan 17, 2025

• instructions

  cos

  committed
  4b8e04b

  Copy full SHA for 4b8e04b