[Move prover] Support explicit cast operation in the spec language for bitvector number types

[rahxephon89]

trafficstars

Description

Prover currently does nothing when using x as u256 in the spec language if x is not a constant. This is not an issue for general number types because they are translated into int in boogie but bv number types are separated: bv8, ...,bv256. This PR adds explicit type conversion for bv number types in the spec language.

How Has This Been Tested?

Existing tests and a new test.

Key Areas to Review

Type of Change

• [x] New feature
• [ ] Bug fix
• [ ] Breaking change
• [ ] Performance improvement
• [ ] Refactoring
• [ ] Dependency update
• [ ] Documentation update
• [ ] Tests

Which Components or Systems Does This Change Impact?

• [ ] Validator Node
• [ ] Full Node (API, Indexer, etc.)
• [ ] Move/Aptos Virtual Machine
• [ ] Aptos Framework
• [ ] Aptos CLI/SDK
• [ ] Developer Infrastructure
• [ ] Move Compiler
• [x] Move prover

Checklist

• [x] I have read and followed the CONTRIBUTING doc
• [x] I have performed a self-review of my own code
• [x] I have commented my code, particularly in hard-to-understand areas
• [x] I identified and added all stakeholders and component owners affected by this change as reviewers
• [x] I tested both happy and unhappy path of the functionality
• [x] I have made corresponding changes to the documentation