[Bug][Prover] Likely Boogie Translation error

[JakeSilverman]

🐛 Bug

Boogie translation error

To reproduce

Replace fungible_asset.spec.move with

spec aptos_framework::fungible_asset {
    spec module {
        // TODO: verification disabled until this module is specified.
    }

    spec unchecked_withdraw {
        modifies global<FungibleStore>(store_addr);
        modifies global<ConcurrentFungibleBalance>(store_addr);
    }

    spec deposit {
        modifies global<FungibleStore>(object::object_address(store));
        modifies global<ConcurrentFungibleBalance>(object::object_address(store));
    }

    spec unchecked_deposit {
        modifies global<FungibleStore>(store_addr);
        modifies global<ConcurrentFungibleBalance>(store_addr);
    }

    spec withdraw_permission_check {
        modifies global<permissioned_signer::PermissionStorage>(permissioned_signer::spec_permission_address(owner));
    }
}

then run env RUST_MIN_STACK=10485760 aptos move prove -f fungible_asset
Stack trace/error message

{
  "Error": "Move Prover failed: [internal] boogie exited with compilation errors:\n/Users/jake/Documents/aptos-core/aptos-move/framework/aptos-framework/boogie.shard_3.bpl(23420,62): Error: use of undeclared function: $1_permissioned_signer_$permission_address\n1 name resolution errors detected in /Users/jake/Documents/aptos-core/aptos-move/framework/aptos-framework/boogie.shard_3.bpl\n"
}

Expected Behavior

Not sure if this will verify, but should not have boogie compilation error.

System information

Please complete the following information:
Aptos Core Version: e1b13f2 (Jul 25 commit)
Rust Version: 1.87.0
Computer OS: macOS 15.5
Boogie version: 3.5.1.0

Additional context

Add any other context about the problem here.

[JakeSilverman]

Can't seem to reproduce, closing for now.