feat: model interior borrows for refcell #786
Conversation
Stevengre
force-pushed
the
jh/mock-spl-data
branch
2 times, most recently
from
f484c1b to
eeab5c0
Compare
Stevengre
changed the title
Co-authored-by: Jost Berthold <[email protected]>
Co-authored-by: Jost Berthold <[email protected]>
dkcumming
left a comment
dkcumming
left a comment
There was a problem hiding this comment.
This is really good work, but I honestly am having a hard time reviewing this as there is a lot happening at once. I tried reading through the whole file and I couldn't get a mental model, and I tried going through each commit but it looks like all your working commits are in there so I see a lot of work that ends up being removed and it is hard to figure out what is changing. In my opinion this needs to be broken up into smaller chunks of work. The Drop semantics would be a nice stand alone PR that can be broken out of this, potentially the ZST information in another. Maybe others can review this effectively but my opinion is this needs to be broken up.
| } | ||
| } | ||
|
|
||
| #[no_mangle] |
There was a problem hiding this comment.
What is the reason for adding no mangle? Is that necessary?
There was a problem hiding this comment.
I added #[no_mangle] so we get a stable symbol name when driving this fixture through the new dylib-based integration test. The harness loads the compiled library and calls lib.get(b"dual_account_demo"); without the attribute that symbol is emitted with the usual Rust mangling (e.g. _RNvNt…dual_account_demo) so the lookup fails. Keeping the unmangled name lets the test resolve the entrypoint consistently. I tried leaning on the mangled name from the metadata, but the crate hash makes that brittle between builds, so the attribute ended up being the reliable fix.
| let account_read = account_info.borrow_data(); | ||
| let mint_read = mint_info.borrow_data(); | ||
| let _ = MiniTokenAccount::unpack_unchecked(&account_read); | ||
| let _ = MiniMint::unpack_unchecked(&mint_read); | ||
| drop(account_read); | ||
| drop(mint_read); | ||
|
|
||
| let mut account_write = account_info.borrow_mut_data(); | ||
| let mut mint_write = mint_info.borrow_mut_data(); | ||
| MiniTokenAccount { | ||
| owner: *b"demoacct", | ||
| amount: 123, | ||
| status: 1, | ||
| } | ||
| .pack_into_slice(&mut account_write); | ||
| MiniMint { | ||
| decimals: 9, | ||
| supply: 500, | ||
| } | ||
| .pack_into_slice(&mut mint_write); |
There was a problem hiding this comment.
It feels like there should be some asserts that the data is as expected after packing and unpacking. It is good to see there is no error but this proof would succeed if the rules were corrupting the data would it not?
There was a problem hiding this comment.
Thanks for catching that! I now re-borrow the account and mint data after packing and assert the unpacked structs match the expected values, so we’ll fail if the rules ever corrupt the data.
| rule #zeroFieldOffset(LAYOUT) | ||
| => #structOffsets(LAYOUT) ==K .MachineSizes | ||
| orBool #structOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes | ||
| orBool #structOffsets(LAYOUT) ==K machineSize(0) .MachineSizes |
There was a problem hiding this comment.
Is this an over approximation or are all of these forms on the RHS of ==K possible?
There was a problem hiding this comment.
I think it's all the possible cases that we need for passing the test.
| rule #typesCompatible(SRC, OTHER) => true | ||
| requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER) |
There was a problem hiding this comment.
So I guess this means that any cast involving a ZST is valid? This is in a section about points to array slices being compatible, I think this needs to be under a ZST section with an explanation
There was a problem hiding this comment.
I followed the current semantics writing style and tried to keep changes simple. Do you mean to move these rules to a separate section with more decriptions?
| rule #zeroSizedType(typeInfoTupleType(.Tys)) => true | ||
| rule #zeroSizedType(typeInfoStructType(_, _, .Tys, _)) => true | ||
| rule #zeroSizedType(_) => false [owise] |
There was a problem hiding this comment.
I don't think this accounts for all the cases, enums and structs containing fields that are only ZSTs are ZSTs themselves, enums with 1 variant, function / closure pointers. I don't expect this PR to implement them all but it should document that the [owise] case is capturing valid ZSTs.
Here is a rust playground to demonstrate
There was a problem hiding this comment.
Thanks for flagging this! Just added a comment under the owise rule.
| syntax Bool ::= #allowsInteriorMutation(TypeInfo) [function, total] | ||
| rule #allowsInteriorMutation(typeInfoStructType(mirString(NAME), _, _, _)) | ||
| => findString(NAME, "UnsafeCell", 0) =/=Int -1 | ||
| rule #allowsInteriorMutation(typeInfoStructType(NAME:String, _, _, _)) | ||
| => findString(NAME, "UnsafeCell", 0) =/=Int -1 | ||
| rule #allowsInteriorMutation(_) => false [owise] |
There was a problem hiding this comment.
Is String matching the best way to do this? It genuinely might be but I feel suspicious of this
There was a problem hiding this comment.
Thanks for calling this out. But I don't know if there any other stable way to find this function rather than String. adtDef is not open and stable to use, I think.
Yes, I totally agree with you. I want this PR to be small at the first time. But since the goal for this pr in my mind is to support concrete execution of |
Stevengre
changed the title
This PR is to support semantics needed by spl-token verification, especially for
RefCellstructure.kmir/src/tests/integration/data/prove-rs/refcell.rs: mock the spl-token domain data access process which providesmainfunction to validate the semantics' concrete support for pack/unpackRefCell<&'a mut [u8]>;dual_account_demofunction to validate the symbolic support.