Skip to content

Multiple Extra Bpl#555

Merged
andrii-a8c merged 4 commits intomainfrom
claude/issue-548-20260306-2006
Mar 10, 2026
Merged

Multiple Extra Bpl#555
andrii-a8c merged 4 commits intomainfrom
claude/issue-548-20260306-2006

Conversation

@andrii-a8c
Copy link
Copy Markdown
Collaborator

@andrii-a8c andrii-a8c commented Mar 10, 2026

Related: #548


Note

Medium Risk
Changes how the prover ingests extra_bpl by allowing multiple files and altering error handling (now continues on invalid paths), plus a broad dependency lockfile update that could affect build/runtime behavior.

Overview
Adds support for specifying multiple extra_bpl attributes on specs/modules by changing validate_and_read_extra_bpl to accept a list of paths, read all valid .bpl files, and concatenate their contents (instead of a single optional file).

Adds integration test cases and snapshots covering both module-level and function-level multi-extra_bpl usage, and updates Cargo.lock with a broad set of dependency bumps (including tokio, rustls, clap, etc.) and new transitive crates.

Written by Cursor Bugbot for commit 2132e5c. This will update automatically on new commits. Configure here.

github-actions bot and others added 3 commits March 6, 2026 20:31
…#548)

Change validate_and_read_extra_bpl to accept &[String] instead of
&Option<String>, iterating over all paths and concatenating contents.
Call sites wrap the current Option<String> into a single-element slice.

Once move-compiler updates VerificationAttribute.extra_bpl from
Option<String> to Vec<String>, call sites change from:
  match extra_bpl { Some(s) => std::slice::from_ref(s), None => &[] }
to:
  extra_bpl.as_slice()

This supports the extra_bpl=b"a.bpl", extra_bpl=b"b.bpl" syntax
once the move-compiler parser accepts duplicate extra_bpl parameters.

Co-authored-by: Andrei Stefanescu <andreistefanescu@users.noreply.github.com>
@andrii-a8c andrii-a8c self-assigned this Mar 10, 2026
Copy link
Copy Markdown
Contributor

@andreistefanescu andreistefanescu left a comment

Choose a reason for hiding this comment

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

👍

Copy link
Copy Markdown

@cursor cursor bot left a comment

Choose a reason for hiding this comment

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

Cursor Bugbot has reviewed your changes and found 1 potential issue.

Bugbot Free Tier Details

Your team is on the Bugbot Free tier. On this plan, Bugbot will review limited PRs each billing cycle for each member of your team.

To receive Bugbot reviews on all of your PRs, visit the Cursor dashboard to activate Pro and start your 14-day free trial.

Bugbot Autofix prepared a fix for the issue found in the latest run.

  • ✅ Fixed: Partial success on error returns incomplete BPL content
    • Updated extra_bpl loading to collect diagnostics but return None if any file validation/read error occurs, preventing partial BPL content from being used.

Create PR

Or push these changes by commenting:

@cursor push f3cb350510
Preview (f3cb350510)
diff --git a/crates/move-stackless-bytecode/src/package_targets.rs b/crates/move-stackless-bytecode/src/package_targets.rs
--- a/crates/move-stackless-bytecode/src/package_targets.rs
+++ b/crates/move-stackless-bytecode/src/package_targets.rs
@@ -764,6 +764,7 @@
         extra_bpl: &Vec<String>,
     ) -> Option<String> {
         let mut contents = Vec::new();
+        let mut has_errors = false;
         for path_str in extra_bpl {
             let extra_path = Path::new(path_str);
 
@@ -773,6 +774,7 @@
                     loc,
                     &format!("extra_bpl path must have .bpl extension: '{}'", path_str),
                 );
+                has_errors = true;
                 continue;
             }
 
@@ -795,6 +797,7 @@
                         resolved_path.display()
                     ),
                 );
+                has_errors = true;
                 continue;
             }
 
@@ -810,10 +813,11 @@
                             err
                         ),
                     );
+                    has_errors = true;
                 }
             }
         }
-        if contents.is_empty() {
+        if has_errors || contents.is_empty() {
             None
         } else {
             Some(contents.join("\n"))

This Bugbot Autofix run was free. To enable autofix for future PRs, go to the Cursor dashboard.

@andrii-a8c andrii-a8c enabled auto-merge (squash) March 10, 2026 18:12
@andrii-a8c andrii-a8c disabled auto-merge March 10, 2026 18:39
@andrii-a8c andrii-a8c merged commit 899b502 into main Mar 10, 2026
16 checks passed
@andrii-a8c andrii-a8c deleted the claude/issue-548-20260306-2006 branch March 10, 2026 18:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants