Pushing Aptos changes upstream #1066

GitOrigin-RevId: c218c01a35bb551a6fbd269b667c3c7aabca4352

GitOrigin-RevId: e28d32f58ea770797ed8e7e6c9fbd75724412950

If there's a generic, the Fat type parsing didn't use the type from the type arguments, which caused it to fail to parse. Now, this will take in the type arguments to properly parse the inputs. GitOrigin-RevId: ba8c0de4e81e23bbe88e7c90ea6356e4c20b5c24

GitOrigin-RevId: 8244cda0130337e8c864f6f6fbc33b0a510e97cf

This introduces the new type of patterns into the model. Patterns are like expressions but represent lvalues or matches. This is used to implement type checking of assignment. Lets also have been refactored to use patterns during checking, but this isn't yet pushed into the AST, which will be a larger breaking change. GitOrigin-RevId: d5c6a8139d96fb16c3fc8bc8d09aaeb28498c57c

GitOrigin-RevId: 51cc46a991d2e2e5445c591ef39da7975f60818a

…lver::Error) and introduce "dyn" instead of "impl" at boundaries (#7817) GitOrigin-RevId: 54f0ce8f8aabac0685174456139e7e2e2ea006cb

…er and simplifier This replaces the use of `LocalVarDecl` accross the model with the new `Pattern` type. This applies to `Block`, `Quant`, and 'Lambda` expression variants. It also removes some code which is currently not used in applications, namely the stackless bytecode interpreter, the spec simplifier and the flattener. While we are refactoring, we have better agility without this code. We can bring it back from git history later if needed. GitOrigin-RevId: a514e89e805b5a5d552c443dd5dad6b5ae117a03

GitOrigin-RevId: 70e6068d2c690209232dbf5896d7ac89496f228f

* refactor a bit * remove arc from VM * Fix is_resource_group * fix build error * temp * tmp * refactor * add utils * remove generic type params * remove unused * revert * fmt * Add new macro * undo changes * improve map_err * remove map_err GitOrigin-RevId: 41cf4715bbfd3a2d7862e810e12ebd1b5d87485d

This reverts commit 41cf4715bbfd3a2d7862e810e12ebd1b5d87485d. GitOrigin-RevId: 04e2662ad9d47b1ecebada305af5376a6575830a

GitOrigin-RevId: b6f79f71b373799d4b21c2e3180119e868320d62

* Revert "Revert "refactor a bit (#7918)"" This reverts commit 04e2662ad9d47b1ecebada305af5376a6575830a. * check * remove cache fallback GitOrigin-RevId: a26b2821feabdc36f83f19f5c16018335daf22a1

* Refactor resolver with metadata * Further refactor * fix api * fix module publishing * make get_resource member of MoveResolver trait * rename remote -> resolver * Address coments * another comment * make session just carry movevm * fix metadata mismatch GitOrigin-RevId: 0e3956259aa7c823e27e16f379d9e63233e6ed6f

GitOrigin-RevId: 0f9891e346180661375e65ef0e1800116cf7e8d7

…t error with storage error GitOrigin-RevId: ebd06050196e4900fe912983453d67f22143d3cb

This is a large refactor of the `move-model` to become independent of bytecode, and an essential step towards the new compiler. In Originally the move-model was designed to work from bytecode as generated by the Move compiler. As such it was input the prover, docgen, and other tools. This PR makes this dependency optional: - The model can still operate base off bytecode, supporting all exisiting use cases and tests. This is important for the incremental introduction of the new compiler infra. - In a new execution path enabled by this PR, the model can also operate without having bytecode as input. In this case, the model builder will completely compile the model from the Move sources. The focus of this PR is preparing the 2nd operation mode without breaking the first. This PR also removes a number of unused crates to simplify refactoring: - stackless bytecode interpreter - legacy read-write set analysis - legacy escape analysis GitOrigin-RevId: eecbcfc1c627048418a0e62e59aa8d69803cc6cd

Move `ChangeSet` and `AccountChangeSet` types are now generic. The motivation for this change is to avoid any particular representation being used to communicate changes. All Move code is fully compatible with the change, all old APIs are preserved. However, additionally session can take a hook which dictates how resources should be outputed. The hook is implemented as a callback which the user can pass on the adapter's side. GitOrigin-RevId: 1e6db1183ec924ca5fe5490e1fd4b571867c150e

GitOrigin-RevId: 65d160be3a168d5dd887eca0218261c881db8808

GitOrigin-RevId: a8ca28437a4ddb1e0f09d8621cf59a2f706c1011

* Add accurate resource group gas metering * Add accurate resource group gas metering * fix * add test * Correct feature version * change trait signature * Clear any resource cache after proloque * bump gas feature * add comment * fix trigger condition for build jobs * test loadtest * add improvement * Fix respawn session whatever that maybe --------- Co-authored-by: gerben <[email protected]> Co-authored-by: geekflyer <[email protected]> GitOrigin-RevId: 09359aa961e909699939783bd438e967ca381bdb

* fix apply schema * fix coin spec * fix trigger condition for build jobs --------- Co-authored-by: geekflyer <[email protected]> GitOrigin-RevId: aaadc26166e57780c01e566cedc1588ecadd9d78

This commit introduces a new fuzzer crate that hosts fuzz tests for aptos-core. The first version of the fuzzer includes these fuzz tests: - Move Bytecode Verifier CodeUnit and Mixed modules - Move execute entry function - Move MoveValue decorate/undecorate - Move MoveValue deserialize - Move Value deserialize - Signed Transaction deserialize GitOrigin-RevId: e267e3ed1f07e1f5a430256854dcff33e71c2263

GitOrigin-RevId: faff4ee44632e772ff6881d12eb5d2eabdf69566

* Fix aptos-labs/aptos-core#7932 Docgen should output attributes (#7932). Output attributes (e.g., #[view] or #[resource_group(scope = global)]) from docgen for move code. Currently only handles attibutes on Function, Script/Module, and Struct/Resource. Note that attributes are allowed on some other syntactic objects (address scope, use statement, const definition, spec), but how to format these usefully in docgen is unclear. for these in docgen is unclear. Also fix an unrelated bug discovered when adapting attribute_placement.move as a test of docgen: previously, only a single Module/Script per input file would be output in docgen. * Update move library docs with new docgen. --------- Co-authored-by: Brian R. Murphy <[email protected]> GitOrigin-RevId: bea5520c277d8e57982798a36c6b60c5aa8bee00

GitOrigin-RevId: 1e65e9703625693801fb335d83fc27690354c2c7

This creates a new crate `move-compiler-v2`, containing a few basic components: - A model of options and experiments for the compiler. This has been adapted from the Move-to-Yul compiler from last year. - A test driver which supports experiments, with a first smoke test to ensure basic functionality of the setup. - Top level entry function to call the compiler. It invokes the new compilation mode of the move-model, which types check and constructs an AST. After that is unimplemented. The PR also adds an additional entry point for the move-model to support the above. GitOrigin-RevId: 1b7b553f3682f1a2ae060e113b4720bfd0799d7e

GitOrigin-RevId: 66de618e4ddb823ca2c2aabaa3726a0e3a43a6eb

GitOrigin-RevId: f4a2a656156071dd162333924e4ec02732d8a27b

GitOrigin-RevId: ad4adbea8c95a82205f22d13058bca9cf433e543

Every tool in Move is now upgraded to clap 4 except for prover GitOrigin-RevId: c4f07e8b73d5ce0acf7847df20ca8cdd0cc73c09

GitOrigin-RevId: a5978350e2d45aff3e75c8698a10102ddbd7db04

This includes putting completions and color into a common crate to be used by any CLI tools GitOrigin-RevId: 8f7ea9a48df70b96fb040ff778dedc6a3773e56d

GitOrigin-RevId: 6c2dcd284629036d86d0a56ed7fea5ae4beee17f

GitOrigin-RevId: ed0b35113acc71acc499c388c62f3d522a97bf01

GitOrigin-RevId: 216c346f7ebccc6ce82a3f5ad945fff2a23a1c36

* [aptos-vm] Add sub_status for error * [aptos-vm] Make groups for sub statuses. GitOrigin-RevId: 76d65fa4bed35a3d15dfa0892ede5b420291dc8a

This extends the compiler driver and testsuite by the basic modules for bytecode generation and processing: - Adds a generator from the Move Model AST to stackless bytecode. This first version only deals with basic expressions. - Configures a stackless bytecode processor pipeline. This will allow us to add multiple phases like safety and borrow analysis and optimizations. For now the pipeline is empty. - Adopts the testsuite to support a test configuration which is configured via the test source directory. This allows us to group tests for testing different aspects of a pipeline. Some of this may look like overkill but this apporach has been worked well for the stackless bytecode processing of the Move Prover. Subsequent PRs will add first processors to the pipeline and iilustrate the usage. GitOrigin-RevId: 7b4aecb3176b8fb7367b65e7fd34a5dac82873b3

GitOrigin-RevId: 54304af41e5b2d2d2aa5210c89f30ca1c98560ca

* initial commit * Support gas payer * Remove relics * Fix * Make verification know about gas payer bit * update comments * Remove merge conflict * Give MSB a good name * Reformat * improve * add comment * Fix spec GitOrigin-RevId: 6d4b49514f1fba0a23c2d515f67b7345ec7c1603

This allows --dev to be added to use the [dev-addresses] as well as updates that really confusing error message to match GitOrigin-RevId: 9b4c616057b234cad468bde2e8539004701752ca

GitOrigin-RevId: 8b5d8548721ad88b166440fb55558bf7d6e5c1cf

The previous dependent dependencies were using an incompatible changes with rust 1.70. This should fix it and condense some of the dependencies. GitOrigin-RevId: c67c15f5bbc5e8d7a65b7d9acabe3fad995f812d

GitOrigin-RevId: 9004a5157fba7380419661c9a223014142f8d646

This PR contains two test cases to show how vector theories might have an impact on the prover's ability on proving complicated propositions w.r.t vector, especially with heavy involvement of quantifiers: - On test case `f1`: - `BoogieArray` (the default vector theory) will given a verification error with an inconsistent counterexample while - `BoogieArrayIntern` and `SmtSeq` can prove the proposition - On test case `f2`: - `BoogieArray` times out while - `BoogieArrayIntern` and `SmtSeq` can prove the proposition GitOrigin-RevId: d3522e12878e7ffbf125cd55bb867ab07838e90e

GitOrigin-RevId: cb39784fad84d6ae32759f3056c9bf7ccddb4a21

…d fixing issues This ports the tests from the v1 compiler for name resolution into the v2 compiler and fixes related issues: - Add support for macros (`assert!`) which are expanded before type checking - Renames and extends the builtin function representation to capture all Move builtins - Distinguishing between symbols defined both in spec and impl or only one of those - Improve error messages - Fixes issues as needed to pass tests GitOrigin-RevId: 691b520464e2fa5927de5807713644a876f676e2

… inlined method. (#8867) Includes test case illustrating original bug (aptos-labs/aptos-core#8516) plus a number of tests to check corner cases of multiple inlining and recursive inlining. (Several failed without this fix.) Also replace panic!("ICE expected function parameter to be a lambda") with a more useful diag output. GitOrigin-RevId: ea19ce1b272e5e2e979057bd58990e76e6c4d03a

* [Spec] add spec to the math modules * Added `math8.move` as the Prover test GitOrigin-RevId: 3d281ad455bd5881c41ae86cd7982b1fa2092cbf

…nline fun declaration. (#8934) (#8958) GitOrigin-RevId: 564f66ad09f3fe26cfa10e63c834c2de69a7ca31

This ports some first batch of 100 test cases from the v1 compiler related to typing, and adapts the implementation to handles those scenarios correctly. - Adds the concept of _constraints_ to type unification. These are basically a first simple version of (for now) builtin traits. For example, a constant `0` has type `X where Constraint::SomePrimitive(u8,u16,..,u256)`. This was needed to match the behavipr of the v1 compiler regards inference related to constants, bu in a more general way. It was not needed previously in the specification language checker because there, we have a unified `num` type for integers. - Implements `&` class of operators in the checker, which weren't supported before. - Cleans up state of the `ExpBuilder` with an `ExpBuilderMode` type instead of multiple booleans. - Multiple smaller improvements, reporting additional errors, making error messages more clearer, etc. GitOrigin-RevId: c8e0581f9b8a8aa1888f118c881a8073d1e5172a

GitOrigin-RevId: c107cbeff4cad50f67ecc49997264bb526029666

* Add stack trace for invariant violation to error message * fmt GitOrigin-RevId: 91bf46d8d639abfce8e3bf5395fdd5dd347cb159

GitOrigin-RevId: 723e57b89a3d24bd94440ab0e0d2632512225751

…hecker This ports the remaining 200+ tests of the v1 compiler `typing` testsuite and refines the v2 compiler to handle those correctly. Major changes include: - Introducing ordering in type unification. This is necessary to deal with conversions like `&mut T` to `&T`. The general mechanism will allow us to have also other conversions if we need down the road. - Introducing a mechanism to define a default for type inference via constraints. If a type variable has no unique instantiation, then the default is chosen. For example, the default for integer constants is `u64`. - Implementing the remaining expansion AST constructs from the Move parser. All expression variants are now handled. With this, we should have a fairly feature complete and tested type checker. This doesn't do, however: - visibility checking (private/friend) - mutation checking (whether something which is mutated can be actually mutated) - ability (copy, drop, ...) checking - reference safety (borrow) checking Those phases have been merged partly into the v1 type checker. For the v2 compiler, the plan is to handle them on bytecode level, similar as in the bytecode verifier. GitOrigin-RevId: b69b4de30cd37f4ca6799c096b6c1069771ba3fd

GitOrigin-RevId: 9510d7896510c4bb179220acfd4bbaf70e544c2b

…erhaul the AST pretty printer for that. GitOrigin-RevId: d0a02371edfbe647d46f99f18e59458831ca3a91

This is a collection of commits submitted to the Aptos version of the Move tree.

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Pushing Aptos changes upstream #1066

Pushing Aptos changes upstream #1066

Commits on Jul 12, 2023