[prover-v2] Connecting Prover to v2 code generation toolchain #12534

wrwg · 2024-03-14T19:51:24Z

This concludes connecting the Move prover to the bytecode generated by the v2 compiler (modulo some remaining issues for which bugs have been opened).

Generates full SourceMap as the prover needs it for error messages
Generates new SpecBlock stackless bytecode instruction for specification blocks, and processes them such that they can be associated by the prover with the bytecode
Plumbs the CLI --compiler-version v2 and MOVE_COMPILER_V2 env var through the spaghetti of aptos cli and Move package system such that v2 compiler is called for model building
Adds a new entry point to the compiler run_move_compiler_for_analysis which builds a model with the v2 compiler for tools like the prover. Also refactors a few other entrypoints in the compiler.
Adds a new flag to prover driver --compiler-v2 to for direct prover invocation. Also adds --aptos for adding Aptos specific prelude in standalone command line mode.
Fixes a bug in the borrow analyis (but also see [prover-v2] Revise borrow analysis #12533)
Adds some verify_duration_estimate pragmas to the framework spec as v2 prover times out (this might be a result of more complex code generated which we should fix down the road with optimizations)
Adds a new test feature to the prover unit tests such that all of them run both against v1 and v2. The v2 exp files are different if it comes to backtracs, which is to be expected with different generated code, but have been compared 1:1 to check whether they are equivalent
Adds a new warning to the prover if intrinsic fields are selected.
Fixes a small bug in reference-safety discovered by the prover tests

trunk-io · 2024-03-14T19:51:28Z

⏱️ 13h 41m total CI duration on this PR

Job	Cumulative Duration	Recent Runs
rust-unit-tests	2h 46m	🟥 ⬜ 🟩 ⬜ 🟩 (+3 more)
windows-build	2h 39m	🟩 🟩 🟩 🟩 🟩 (+4 more)
rust-move-tests	2h 2m	🟥 ⬜ 🟩 ⬜ 🟩 (+3 more)
rust-move-unit-coverage	1h 58m	🟩 ⬜ 🟩 ⬜ 🟩 (+3 more)
rust-lints	49m	🟥 ⬜ 🟩 ⬜ 🟩 (+3 more)
run-tests-main-branch	33m	🟥 🟥 🟥 🟩 🟩 (+3 more)
rust-smoke-tests	33m	🟩
check	29m	🟩 🟩 ⬜ ⬜ 🟩 (+4 more)
execution-performance / single-node-performance	24m	🟩
check-dynamic-deps	18m	🟩 🟩 🟩 🟩 🟩 (+4 more)
general-lints	16m	🟩 🟩 🟩 ⬜ 🟩 (+3 more)
forge-e2e-test / forge	14m	🟩
rust-images / rust-all	14m	🟩
forge-compat-test / forge	12m	🟩
cli-e2e-tests / run-cli-tests	6m	🟩
semgrep/ci	3m	🟩 🟩 🟩 🟩 🟩 (+4 more)
file_change_determinator	1m	🟩 🟩 🟩 ⬜ 🟩 (+4 more)
file_change_determinator	1m	🟩 🟩 🟩 🟩 🟩 (+3 more)
node-api-compatibility-tests / node-api-compatibility-tests	52s	🟩
permission-check	29s	🟩 🟩 🟩 🟩 🟩 (+4 more)
permission-check	28s	🟩 🟩 🟩 🟩 🟩 (+4 more)
permission-check	25s	🟩 🟩 🟩 🟩 🟩 (+4 more)
permission-check	25s	🟩 🟩 🟩 🟩 🟩 (+4 more)
execution-performance / file_change_determinator	10s	🟩
file_change_determinator	8s	🟩
permission-check	2s	🟩
determine-docker-build-metadata	2s	🟩

_{settings ⋅ feedback ⋅ docs ⋅ learn more about trunk.io}

codecov · 2024-03-14T20:11:02Z

Codecov Report

Attention: Patch coverage is 75.71429% with 119 lines in your changes are missing coverage. Please review.

Project coverage is 64.1%. Comparing base (e2fd0ba) to head (221845a).
Report is 1 commits behind head on main.

Files	Patch %	Lines
...ools/move-package/src/compilation/model_builder.rs	21.6%	29 Missing ⚠️
third_party/move/move-model/src/ast.rs	54.7%	24 Missing ⚠️
third_party/move/move-compiler-v2/src/lib.rs	76.0%	18 Missing ⚠️
third_party/move/move-model/src/model.rs	62.9%	10 Missing ⚠️
...e-prover/boogie-backend/src/bytecode_translator.rs	53.8%	6 Missing ⚠️
...ty/move/move-model/bytecode/src/borrow_analysis.rs	66.6%	5 Missing ⚠️
third_party/move/tools/move-cli/src/base/docgen.rs	0.0%	5 Missing ⚠️
...iler-v2/src/pipeline/livevar_analysis_processor.rs	42.8%	4 Missing ⚠️
...model/bytecode/src/stackless_bytecode_generator.rs	33.3%	4 Missing ⚠️
...ty/move/move-model/bytecode/src/function_target.rs	84.2%	3 Missing ⚠️
... and 7 more

Additional details and impacted files

@@           Coverage Diff            @@
##             main   #12534    +/-   ##
========================================
  Coverage    64.0%    64.1%            
========================================
  Files         818      818            
  Lines      181627   181930   +303     
========================================
+ Hits       116377   116649   +272     
- Misses      65250    65281    +31

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

brmataptos

You should consider moving the 2 flagged changes to move semantics to a separate PR so they can have a distinct commit message explaining what they're about.

brmataptos · 2024-03-18T21:07:28Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

@@ -35,6 +39,8 @@ pub struct FunctionGenerator<'a> {
    locals: Vec<Type>,
    /// A map from branching labels to information about them.
    label_info: BTreeMap<Label, LabelInfo>,
+    /// A mao from code offset to spec blocks associated with them


brmataptos · 2024-03-18T21:13:36Z

third_party/move/move-prover/tests/testsuite.rs

+                name: "v2",
+                flags: &[],
+                inclusion_mode: InclusionMode::Implicit,
+                enable_in_ci: true,


Setting enable_in_ci to true seems questionable. Before it was disabled with comment "Do not enable in CI until we have more data about stability". Do we have that stability data now?

brmataptos · 2024-03-18T21:45:48Z

third_party/move/move-model/src/model.rs

+    /// the difference between targets and dependencies for verification.
+    /// Those tools can temporarily set this to true.
+    pub fn treat_everything_as_target(&self, on: bool) {
+        *self.everything_is_target.borrow_mut() = on


Please file an issue to do something to clean this up eventually (much later). For example, we may want to shake the tree and only include the dependences which are reachable from the original targets. Or we might want to distinguish the different levels (to be compiled, to be generated as code, to be included as needed). The mutable nature here is not ideal, as it could be dangerous in the long term. But it's fine for now.

We are already minimizing the tree in the module_builder somewhere. For the other issue see above.

brmataptos · 2024-03-18T21:57:57Z

third_party/move/move-model/bytecode/src/borrow_analysis.rs

                    },
-                    AssignKind::Store => {
+                    AssignKind::Copy | AssignKind::Store => {


*** This (adding an edge for AssignKind::Copy) seems to be a significant change for borrow analysis. Might be better to give it its own commit/PR so it can have a reason attached.

Yes, that is why I opened #12533.

brmataptos · 2024-03-18T22:00:31Z

third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs

@@ -1012,7 +1012,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
    fn check_borrow_safety(&mut self, temps_vec: &[TempIndex]) {
        // First check direct duplicates
        for (i, temp) in temps_vec.iter().enumerate() {
-            if temps_vec[i + 1..].contains(temp) {
+            if self.ty(*temp).is_mutable_reference() && temps_vec[i + 1..].contains(temp) {


*** This also is a pretty big deal for borrow analysis.

Yes, it was a serious bug. The one-and-only the prover integration found so far.

brmataptos · 2024-03-18T22:04:36Z

third_party/move/move-compiler-v2/src/lib.rs

+    error_writer: &mut impl WriteColor,
+    mut options: Options,
+) -> anyhow::Result<GlobalEnv> {
+    options.whole_program = true; // will set `treat_everything_as_target`


"Everything as target" is probably not is wanted in the general analysis case. Our various compiler warning checks need to know the difference between "warn about this code" and "don't warn about this code". Currently they are using "target" to decide whether to warn about code, but for certain targeted analyses you would want to do different things for "real target" and "target because it's a dependency". That may mean we just need a new flag for "generate warnings/errors about this code".

You usually expect that the prover is run an code which already passes type checks. But if not, we can't really differentiate whether the type check error is in the set targets or not, so we better produce errors in the dependencies as well. I think a really sustainable solution for the problem is that the package system somehow tracks this for us and/or we have some on-disk storage of compiled packages. Keeping for now like this until we have a better solution, perhaps after package system refactoring.

brmataptos · 2024-03-18T22:30:17Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

+                Bytecode::SpecBlock(_, spec) => {
+                    // All Temporaries used in the spec need to be pinned. Notice that
+                    // any bound variables inside the spec are LocalVar, so we can just
+                    // unconditionally collect them.


them --> all Temporary vars

brmataptos · 2024-03-18T22:47:03Z

aptos-move/framework/move-stdlib/doc/features.md

Does this have anything to do with your change, or was it just not regenerated recently?

Please do not look at md which is generated but at the Move source of the same name. There is a bug linked there already and a TODO (#12501).

brmataptos · 2024-03-18T22:47:17Z

aptos-move/framework/aptos-framework/doc/staking_config.md

This one too, does it have any relevance, or was it just stale before?

Please comment on the .move source, this here is generated.

This was a test which was borderline regards timeout, and clearly times out with v2, I deactivated for CI using the pragma as here, as we do in many cases.

brmataptos · 2024-03-18T22:59:32Z

third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs

@@ -846,4 +865,12 @@ impl<'env> ModuleContext<'env> {
        }
        result
    }
+
+    /// Converts to a name with location as expected by the SourceMap format.
+    pub(crate) fn source_name(&self, name: impl AsRef<Symbol>, loc: impl AsRef<Loc>) -> SourceName {


Are we expecting some other things that will be convertable to &Symbol that might show up here? I realize AsRef<Loc> was already fairly common in the code, and AsRef<str> is very useful in Rust, but do we anticipate other implementations that would warrant slightly more complex code here?

Its really just about references, and we should have used it more frequently. With this you are able to pass parameters without * or &. We often need to do * because in matches, we get &Symbol. Similar for locations, we often need to add &. This reduces the noise a bit.

vineethk

Have some comments, but none of them blocking (but would be good to address/answer). I did not check the test outputs for the move prover, so someone from the prover team might be better equipped to review these.

vineethk · 2024-03-20T13:55:43Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

 };
 use std::collections::{BTreeMap, BTreeSet};

 pub struct FunctionGenerator<'a> {
    /// The underlying module generator.
    gen: &'a mut ModuleGenerator,
    /// The set of temporaries which need to be pinned to locals because references are taken for
-    /// them.
+    /// them, or they are used in specs.


Interesting, this would mean that codegen quality could be affected solely by the presence of a use in specs (which is typically expected to be a no-op for compilation). Might be worth re-considering this as a future task.

Yes, but this was always the case, also in v1.

We could actually make this optional depending on whether we generate code for the prover or not, but the problem with this is that then we wouldn't verify the same bytecode as it is running in production.

Not suggesting that we do this now, but another alternative is to transform the specs as we transform the normal code.

vineethk · 2024-03-20T14:01:30Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

@@ -211,8 +240,22 @@ impl<'a> FunctionGenerator<'a> {
    fn pinned_temps(ctx: &FunctionContext) -> BTreeSet<TempIndex> {
        let mut result = BTreeSet::new();
        for bc in ctx.fun.get_bytecode() {
-            if let Bytecode::Call(_, _, Operation::BorrowLoc | Operation::Drop, args, _) = bc {
-                result.insert(args[0]);
+            match bc {


Update the function doc (which says this is getting temps referenced in borrow instructions, but now it does more).

vineethk · 2024-03-20T14:05:19Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

+    /// locals. The spec block is then stored in the spec block table
+    /// which will be written back to the function spec at the end of
+    /// translation. In the actual Move bytecode, a `Nop` is inserted
+    /// at the current code offset.


Curious: why do we need to insert a no-op, instead of not emitting anything?

It's a convention the v1 compiler is using. It makes it easier to identify that this is a gluing point for specs and can be used e.g. in program analysis if some extra spec related info is generated for this program point.

vineethk · 2024-03-20T14:12:24Z

third_party/move/move-compiler-v2/src/file_format_generator/module_generator.rs

        let struct_handle = self.struct_index(ctx, loc, struct_env);
+        let fields = struct_env
+            .get_fields()
+            .sorted_by(|a, b| a.get_offset().cmp(&b.get_offset()));


From looking at the code for get_fields(), it looks like they are already sorted based on their offsets?

Good catch, fixed.

vineethk · 2024-03-20T14:32:08Z

third_party/move/move-model/bytecode/src/borrow_analysis.rs

-                        assert!(!self.func_target.get_local_type(*src).is_reference());
-                        assert!(!self.func_target.get_local_type(*dest).is_reference());
+                        if self.func_target.get_local_type(*src).is_mutable_reference() {
+                            assert!(self


Might be worth stating that this assertion holds because we are supposed to have inserted freezerefs when converting from &mut to & everywhere already?

Frankly, I don't even know were this assumption comes from and whether it is needed (this is a duplicate of few lines below). In general I opened #12533 to follow up here.

vineethk · 2024-03-20T14:45:05Z

third_party/move/move-model/src/lib.rs

@@ -511,7 +523,7 @@ pub fn add_move_lang_diagnostics(env: &mut GlobalEnv, diags: Diagnostics) {
 }

 #[allow(deprecated)]


Check if we are still using something here that is deprecated.

Yeah, we should remove this deprecation, some guy added it years ago not knowing the prover needs it.

vineethk · 2024-03-20T14:57:53Z

third_party/move/move-compiler-v2/tests/ability-transform/mutate_return.exp

@@ -1,11 +1,5 @@
 ============ initial bytecode ================


Have not looked into why the ordering changed - maybe worth a brief look whether this is an acceptable change?

I'm also surprised why, but it doesn't hurt, so...

vineethk · 2024-03-20T15:18:21Z

third_party/move/move-compiler-v2/tests/bytecode-verify-failure/equality.exp

-4 │ │     }
-5 │ │ }
-  │ ╰─^ ICE failed bytecode verifier: VMError {
+3 │         x == y


I think you have also fixed this bug: #11925. If you think so too, maybe close that bug through this PR.

Actually not, it is only that error message is more precise because I now generate the full source map.

vineethk · 2024-03-20T15:22:33Z

third_party/move/move-compiler-v2/src/pipeline/reference_safety_processor.rs

@@ -1012,7 +1012,7 @@ impl<'env, 'state> LifetimeAnalysisStep<'env, 'state> {
    fn check_borrow_safety(&mut self, temps_vec: &[TempIndex]) {
        // First check direct duplicates
        for (i, temp) in temps_vec.iter().enumerate() {
-            if temps_vec[i + 1..].contains(temp) {
+            if self.ty(*temp).is_mutable_reference() && temps_vec[i + 1..].contains(temp) {
                self.exclusive_access_direct_dup_error(*temp)


If a test case corresponding to this (eg, call to a function with multiple dup args that are non-mut references) has not been added, please do.

Done, new test is duplicate_use.move

vineethk · 2024-03-20T15:24:30Z

...move/move-compiler-v2/transactional-tests/tests/no-v1-comparison/access_control/negation.exp

@@ -13,7 +13,7 @@ Error: Function execution failed with VMError: {
    sub_status: None,
    location: 0x42::test,
    indices: [],
-    offsets: [(FunctionDefinitionIndex(0), 1)],
+    offsets: [(FunctionDefinitionIndex(1), 1)],


Likely okay, but good to double check if this ordering change is known and acceptable.

I checked its semantically the same, so at this point, I just let it go. If it is an issue like some hidden non-determinism we will detect soon anyway.

wrwg

Thanks for the review.

wrwg · 2024-03-20T18:44:19Z

aptos-move/framework/move-stdlib/doc/features.md

Please do not look at md which is generated but at the Move source of the same name. There is a bug linked there already and a TODO (#12501).

wrwg · 2024-03-20T18:46:45Z

aptos-move/framework/aptos-framework/doc/staking_config.md

Please comment on the .move source, this here is generated.

This was a test which was borderline regards timeout, and clearly times out with v2, I deactivated for CI using the pragma as here, as we do in many cases.

wrwg · 2024-03-20T18:51:09Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

 };
 use std::collections::{BTreeMap, BTreeSet};

 pub struct FunctionGenerator<'a> {
    /// The underlying module generator.
    gen: &'a mut ModuleGenerator,
    /// The set of temporaries which need to be pinned to locals because references are taken for
-    /// them.
+    /// them, or they are used in specs.


Yes, but this was always the case, also in v1.

We could actually make this optional depending on whether we generate code for the prover or not, but the problem with this is that then we wouldn't verify the same bytecode as it is running in production.

wrwg · 2024-03-20T18:51:27Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

@@ -35,6 +39,8 @@ pub struct FunctionGenerator<'a> {
    locals: Vec<Type>,
    /// A map from branching labels to information about them.
    label_info: BTreeMap<Label, LabelInfo>,
+    /// A mao from code offset to spec blocks associated with them


wrwg · 2024-03-20T18:52:21Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

@@ -211,8 +240,22 @@ impl<'a> FunctionGenerator<'a> {
    fn pinned_temps(ctx: &FunctionContext) -> BTreeSet<TempIndex> {
        let mut result = BTreeSet::new();
        for bc in ctx.fun.get_bytecode() {
-            if let Bytecode::Call(_, _, Operation::BorrowLoc | Operation::Drop, args, _) = bc {
-                result.insert(args[0]);
+            match bc {


wrwg · 2024-03-20T19:24:14Z

third_party/move/move-model/bytecode/src/borrow_analysis.rs

-                        assert!(!self.func_target.get_local_type(*src).is_reference());
-                        assert!(!self.func_target.get_local_type(*dest).is_reference());
+                        if self.func_target.get_local_type(*src).is_mutable_reference() {
+                            assert!(self


Frankly, I don't even know were this assumption comes from and whether it is needed (this is a duplicate of few lines below). In general I opened #12533 to follow up here.

wrwg · 2024-03-20T19:24:33Z

third_party/move/move-model/bytecode/src/borrow_analysis.rs

                    },
-                    AssignKind::Store => {
+                    AssignKind::Copy | AssignKind::Store => {


Yes, that is why I opened #12533.

wrwg · 2024-03-20T19:28:00Z

third_party/move/move-model/bytecode/src/stackless_bytecode.rs

@@ -519,6 +522,10 @@ impl Bytecode {
            | Bytecode::Nop(_) => {
                vec![]
            },
+            Bytecode::SpecBlock(_, _) => {
+                // Specifications are not contributing to read variables


Yes, but as long as we do not eliminate the temporaries, lifetime doesn't matter for the prover. We need to take care of pinning them similar as we do with borrows of locals. If one your optimizations needs this pinning, please let me know and we can have a followup PR to fix this.

wrwg · 2024-03-20T19:28:52Z

third_party/move/move-model/src/lib.rs

@@ -511,7 +523,7 @@ pub fn add_move_lang_diagnostics(env: &mut GlobalEnv, diags: Diagnostics) {
 }

 #[allow(deprecated)]


Yeah, we should remove this deprecation, some guy added it years ago not knowing the prover needs it.

wrwg · 2024-03-20T19:31:03Z

third_party/move/move-model/src/model.rs

+    /// the difference between targets and dependencies for verification.
+    /// Those tools can temporarily set this to true.
+    pub fn treat_everything_as_target(&self, on: bool) {
+        *self.everything_is_target.borrow_mut() = on


We are already minimizing the tree in the module_builder somewhere. For the other issue see above.

vineethk · 2024-03-20T19:50:57Z

@wrwg You probably already saw this, but it looks like "Aptos Move Test for Compiler V2" is failing (and it is not required, so easy to see past it).

wrwg · 2024-03-20T22:31:12Z

@wrwg You probably already saw this, but it looks like "Aptos Move Test for Compiler V2" is failing (and it is not required, so easy to see past it).

Yes, thank you @vineethk . There were a few tests failing after rebasing with various optimizations on. As I guessed, pinning spec locals for variable coalescing and considering for lifetime in the case of dead store elimination needed to be done. If you want, please check the last commit, as it effects some of the code you have written.

vineethk

Added some comments for the latest commit.

vineethk · 2024-03-20T22:47:12Z

third_party/move/move-compiler-v2/src/file_format_generator/function_generator.rs

 };
 use std::collections::{BTreeMap, BTreeSet};

 pub struct FunctionGenerator<'a> {
    /// The underlying module generator.
    gen: &'a mut ModuleGenerator,
    /// The set of temporaries which need to be pinned to locals because references are taken for
-    /// them.
+    /// them, or they are used in specs.


Not suggesting that we do this now, but another alternative is to transform the specs as we transform the normal code.

vineethk · 2024-03-20T22:53:56Z

third_party/move/move-compiler-v2/src/pipeline/livevar_analysis_processor.rs

-                for (idx, _) in exp.used_temporaries(self.func_target.global_env()) {
+            Prop(id, _, exp) if self.track_all_usages => {
+                for idx in exp.used_temporaries() {
+                    state.livevars.insert(idx, self.livevar_info(id, offset));


I think this should be state.insert_or_update so that we join rather than replace (which is what insert would do)?

vineethk · 2024-03-20T22:56:28Z

third_party/move/move-compiler-v2/src/pipeline/avail_copies_analysis.rs

@@ -217,7 +217,7 @@ impl FunctionTargetProcessor for AvailCopiesAnalysisProcessor {
            return data;
        }
        let target = FunctionTarget::new(func_env, &data);
-        let analysis = AvailCopiesAnalysis::new(target.get_borrowed_locals());
+        let analysis = AvailCopiesAnalysis::new(target.get_pinned_temps(false));


Search and replace borrowed with pinned in this file.

This concludes connecting the Move prover to the bytecode generated by the v2 compiler (modulo some remaining issues for which bugs have been opened). - Generates full SourceMap as the prover needs it for error messages - Generates new `SpecBlock` stackless bytecode instruction for specification blocks, and processes them such that they can be associated by the prover with the bytecode - Plumbs the CLI `--compiler-version v2` and `MOVE_COMPILER_V2` env var through the spaghetti of aptos cli and Move package system such that v2 compiler is called for model building - Adds a new entry point to the compiler `run_move_compiler_for_analysis` which builds a model with the v2 compiler for tools like the prover. Also refactors a few other entrypoints in the compiler. - Adds a new flag to prover driver `--compiler-v2` to for direct prover invocation. Also adds `--aptos` for adding Aptos specific prelude in standalone command line mode. - Fixes a bug in the borrow analyis (but also see #12533) - Adds some `verify_duration_estimate` pragmas to the framework spec as v2 prover times out (this might be a result of more complex code generated which we should fix down the road with optimizations) - Adds a new test feature to the prover unit tests such that all of them run both against v1 and v2. The v2 exp files are different if it comes to backtracs, which is to be expected with different generated code, but have been compared 1:1 to check whether they are equivalent - Fixes a small bug in reference-safety discovered by the prover tests

- Needed to pin temps for variable coalascing. This has been done by making `get_pinned_temps` a shared function between coalascing and function generator - Needed to consider spec temp usages if `track_all_targets` is set in LiveVarAnalysis. This is needed so dead store elimination does not remove assignments used in specs. - Renamed `used_temporaries` to `used_temporaries_with_types` and let the original function work without global env and delivering types, so it can be used in places were no env is available. - Make `MOVE_COMPILER_V2` turn on compiler v2 also for prover runs - Extended `move_pr.sh` with a new option `-2` which makes it run all integration tests v2, as we do on github

github-actions · 2024-03-21T01:32:46Z

✅ Forge suite `compat` success on `aptos-node-v1.9.5` ==> `221845afa301b5f84573e33d6ec11a2998a42b4f`

Compatibility test results for aptos-node-v1.9.5 ==> 221845afa301b5f84573e33d6ec11a2998a42b4f (PR)
1. Check liveness of validators at old version: aptos-node-v1.9.5
compatibility::simple-validator-upgrade::liveness-check : committed: 5527 txn/s, latency: 5719 ms, (p50: 4800 ms, p90: 9800 ms, p99: 14400 ms), latency samples: 210040
2. Upgrading first Validator to new version: 221845afa301b5f84573e33d6ec11a2998a42b4f
compatibility::simple-validator-upgrade::single-validator-upgrade : committed: 720 txn/s, latency: 34041 ms, (p50: 36700 ms, p90: 51300 ms, p99: 54300 ms), latency samples: 58340
3. Upgrading rest of first batch to new version: 221845afa301b5f84573e33d6ec11a2998a42b4f
compatibility::simple-validator-upgrade::half-validator-upgrade : committed: 262 txn/s, submitted: 586 txn/s, expired: 324 txn/s, latency: 32327 ms, (p50: 38100 ms, p90: 55600 ms, p99: 57500 ms), latency samples: 22587
4. upgrading second batch to new version: 221845afa301b5f84573e33d6ec11a2998a42b4f
compatibility::simple-validator-upgrade::rest-validator-upgrade : committed: 2021 txn/s, latency: 14900 ms, (p50: 18100 ms, p90: 20800 ms, p99: 22900 ms), latency samples: 95020
5. check swarm health
Compatibility test for aptos-node-v1.9.5 ==> 221845afa301b5f84573e33d6ec11a2998a42b4f passed
Test Ok

github-actions · 2024-03-21T01:34:31Z

✅ Forge suite `realistic_env_max_load` success on `221845afa301b5f84573e33d6ec11a2998a42b4f`

two traffics test: inner traffic : committed: 7116 txn/s, latency: 5504 ms, (p50: 5400 ms, p90: 6600 ms, p99: 10400 ms), latency samples: 3081540
two traffics test : committed: 100 txn/s, latency: 1874 ms, (p50: 1800 ms, p90: 2100 ms, p99: 4300 ms), latency samples: 1800
Latency breakdown for phase 0: ["QsBatchToPos: max: 0.230, avg: 0.203", "QsPosToProposal: max: 0.356, avg: 0.314", "ConsensusProposalToOrdered: max: 0.522, avg: 0.464", "ConsensusOrderedToCommit: max: 0.305, avg: 0.286", "ConsensusProposalToCommit: max: 0.770, avg: 0.750"]
Max round gap was 1 [limit 4] at version 1380866. Max no progress secs was 4.119738 [limit 15] at version 1380866.
Test Ok

wrwg requested review from vineethk, junkil-park, rahxephon89, fEst1ck and brmataptos March 14, 2024 19:51

wrwg requested review from gregnazario, banool, davidiw and movekevin as code owners March 14, 2024 19:51

wrwg force-pushed the wrwg/v2-prover branch from dda40e8 to ca0e31b Compare March 14, 2024 23:00

wrwg mentioned this pull request Mar 14, 2024

[compiler-v2] Disassembler doesn't work with source map constructed by the compiler #12541

Closed

wrwg force-pushed the wrwg/v2-prover branch from ca0e31b to 6fa6cfa Compare March 15, 2024 00:00

brmataptos approved these changes Mar 18, 2024

View reviewed changes

vineethk approved these changes Mar 20, 2024

View reviewed changes

wrwg mentioned this pull request Mar 20, 2024

[prover-v2] Revise borrow analysis #12533

Closed

wrwg commented Mar 20, 2024

View reviewed changes

wrwg force-pushed the wrwg/v2-prover branch from 6fa6cfa to 6ac6638 Compare March 20, 2024 19:52

wrwg force-pushed the wrwg/v2-prover branch from cf05f72 to e79bf2a Compare March 20, 2024 22:36

vineethk reviewed Mar 20, 2024

View reviewed changes

wrwg force-pushed the wrwg/v2-prover branch from e79bf2a to 622caef Compare March 21, 2024 01:05

wrwg added 3 commits March 20, 2024 18:05

Addressing reviewer comments

a14b583

wrwg force-pushed the wrwg/v2-prover branch from 622caef to 221845a Compare March 21, 2024 01:05

wrwg enabled auto-merge (squash) March 21, 2024 01:05

This comment has been minimized.

Sign in to view

wrwg merged commit 8317487 into main Mar 21, 2024
73 checks passed

wrwg deleted the wrwg/v2-prover branch March 21, 2024 01:39

vineethk mentioned this pull request Mar 22, 2024

[Bug][compiler-v2] Location information in bytecode verification bugs could be improved #11925

Closed

vineethk mentioned this pull request Dec 4, 2024

[compiler-v2] Do not include vector module for compiler v1 #15484

Merged

2 tasks

		@@ -511,7 +523,7 @@ pub fn add_move_lang_diagnostics(env: &mut GlobalEnv, diags: Diagnostics) {
		}

		#[allow(deprecated)]

		@@ -1,11 +1,5 @@
		============ initial bytecode ================

[prover-v2] Connecting Prover to v2 code generation toolchain #12534

[prover-v2] Connecting Prover to v2 code generation toolchain #12534

Conversation

wrwg commented Mar 14, 2024

trunk-io bot commented Mar 14, 2024 • edited Loading

codecov bot commented Mar 14, 2024 • edited Loading

Codecov Report

brmataptos left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vineethk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

wrwg left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

vineethk commented Mar 20, 2024

wrwg commented Mar 20, 2024

vineethk left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

This comment has been minimized.

This comment has been minimized.

github-actions bot commented Mar 21, 2024

✅ Forge suite compat success on aptos-node-v1.9.5 ==> 221845afa301b5f84573e33d6ec11a2998a42b4f

github-actions bot commented Mar 21, 2024

✅ Forge suite realistic_env_max_load success on 221845afa301b5f84573e33d6ec11a2998a42b4f

trunk-io bot commented Mar 14, 2024 •

edited

Loading

codecov bot commented Mar 14, 2024 •

edited

Loading

✅ Forge suite `compat` success on `aptos-node-v1.9.5` ==> `221845afa301b5f84573e33d6ec11a2998a42b4f`

✅ Forge suite `realistic_env_max_load` success on `221845afa301b5f84573e33d6ec11a2998a42b4f`