How to include multiple extra BPL files?

[msaaltink]

There should be a way to ask for multiple extra_bpl files to be used.

When a module has more than one extra_bpl attribute, only the last of them is effective.
For example here:

#[spec_only(extra_bpl=b"a.bpl", extra_bpl=b"b.bpl")]
module two_extra::two_extra;

native fun a(x: u8): u8;

native fun b(x: u8): u8;

#[spec(prove)]
fun test() {
    prover::prover::ensures(a(0) == b(1));
}

where
a.bpl says

procedure {:inline 1} $0_two_extra_a(x: int) returns (r: int) { r := 0; }

and b.bpl says

procedure {:inline 1} $0_two_extra_b(x: int) returns (r: int) { r := 0; }

The prover gives

boogie exited with compilation errors:
output/two_extra::test_Check.bpl(4380,4): Error: call to undeclared procedure: $0_two_extra_a

In this specific case, the workaround is to place

#[spec(prove, extra_bpl=b"a.bpl")]

before the function, but that fails if there are three or more files to include.

If the line before function test is changed to
#[spec(prove, extra_bpl=b"a.bpl", extra_bpl=b"a.bpl")]
giving

#[spec_only]
module two_extra::two_extra;

native fun a(x: u8): u8;

native fun b(x: u8): u8;


#[spec(prove, extra_bpl=b"a.bpl", extra_bpl=b"a.bpl")]
fun test() {
    prover::prover::ensures(a(0) == b(1));
}

we get

error: invalid attribute
   ┌─ ./sources/two_extra.move:10:3
   │
10 │ #[spec(prove, extra_bpl=b"a.bpl", extra_bpl=b"a.bpl")]
   │   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ Duplicate spec parameter 'extra_bpl'

I tried separating pathnames with spaces or commas, (e.g., extra_bpl=b"a.bpl,b.bpl") but that did not work either.

[andreistefanescu]

@claude try to fix this

[claude]

Claude finished @andreistefanescu's task in 10m 14s —— View job • claude/issue-548-20260306-1949 • Create PR ➔

---

Fix for multiple extra_bpl files support

• Gather context - explored codebase for extra_bpl handling
• Understand the request and plan the fix
• Implement: modified validate_and_read_extra_bpl in package_targets.rs to split on commas and read all files
• Add test files for multiple extra_bpl (function-level and module-level)
• Verified existing failure tests pass (no regressions)
• Commit and push changes

Summary

Root cause: The extra_bpl attribute is stored as Option<String> in the move-compiler dependency. With the existing implementation, only a single file path could be specified per attribute, and using duplicate attribute keys was either silently ignored (module-level) or caused a "Duplicate spec parameter" error (function-level).

Fix: Modified validate_and_read_extra_bpl in crates/move-stackless-bytecode/src/package_targets.rs to support comma-separated paths. Users can now write:

// Function-level (2 or more files)
#[spec(prove, extra_bpl = b"a.bpl,b.bpl")]
fun test() { ... }

// Module-level (2 or more files)
#[spec_only(extra_bpl = b"a.bpl,b.bpl")]
module my_module;

The function now splits the input on commas, trims whitespace around each path, validates the .bpl extension, resolves relative paths, reads each file, and concatenates the contents.

This matches what the issue reporter expected to work (extra_bpl=b"a.bpl,b.bpl").

|

[andreistefanescu]

@claude do extra_bpl=b"a.bpl", extra_bpl=b"a.bpl", not extra_bpl=b"a.bpl,b.bpl"

[claude]

Claude finished @andreistefanescu's task in 25m 25s —— View job • claude/issue-548-20260306-2006 • Create PR ➔

---

Changes implemented for multiple extra_bpl support

• Gather context and analyze requirements
• Understand root cause: extra_bpl is Option<String> in VerificationAttribute (move-compiler)
• Implement: change validate_and_read_extra_bpl to accept &[String], iterate all paths, concatenate
• Update all 3 call sites with backward-compatible Option<String> → &[String] conversion
• Commit and push

Summary

What this PR does: Refactors validate_and_read_extra_bpl in package_targets.rs to accept &[String] instead of &Option<String>, so it can handle multiple BPL files by iterating over all paths and concatenating their contents.

What's needed in asymptotic-code/sui: Supporting extra_bpl=b"a.bpl", extra_bpl=b"b.bpl" requires two changes to move-compiler/src/shared/known_attributes.rs:

1. Change extra_bpl: Option<String> → extra_bpl: Vec<String> in VerificationAttribute::SpecOnly and VerificationAttribute::Spec
2. Update the parser to collect all extra_bpl values into the Vec (instead of last-wins for spec_only, or rejecting duplicates for spec)

Migration: Once move-compiler is updated, the 3 call sites in package_targets.rs change from:

let extra_bpl_paths: &[String] = match extra_bpl {
    Some(s) => std::slice::from_ref(s),
    None => &[],
};

to simply:

let extra_bpl_paths: &[String] = extra_bpl.as_slice();

| claude/issue-548-20260306-2006

[andreistefanescu]

fixed in #555.