Skip to content
Closed
Changes from 1 commit
Commits
Show all changes
66 commits
Select commit Hold shift + click to select a range
8a72058
chore: add test for std refcell
Stevengre Oct 29, 2025
9f82eec
chore: add simple test for one struct casting
Stevengre Oct 30, 2025
c2d6862
chore: update state without thunk and any modification
Stevengre Oct 30, 2025
28cf9d5
feat: support UnsafeCell cast to Int
Stevengre Oct 30, 2025
93cad6f
chore: new passed prove-rs/local-raw-fail.rs test
Stevengre Oct 30, 2025
fa24d9b
fix: closure_access_struct failure
Stevengre Oct 30, 2025
ede664c
chore: make format
Stevengre Oct 30, 2025
55237eb
chore: remove passed test expected
Stevengre Oct 30, 2025
21f5034
chore: update expected state
Stevengre Oct 30, 2025
537b584
chore: update test pass status
Stevengre Oct 30, 2025
c525218
chore: update test pass status
Stevengre Oct 30, 2025
f270fe8
chore: add more test for the semantics
Stevengre Oct 31, 2025
c25f259
chore: update test_integration.py
Stevengre Oct 31, 2025
2093f58
feat: support reverse transparent struct cast
Stevengre Nov 1, 2025
a313ead
feat: refine transparent alignment handling
Stevengre Nov 3, 2025
1057a44
update expected output
Stevengre Nov 3, 2025
d3d93ca
feat: solve interior-mut3-fail.rs
Stevengre Nov 4, 2025
8d95126
feat: provide more information for functions without body
Stevengre Nov 4, 2025
46e791a
feat(not-ready)
Stevengre Nov 4, 2025
4b3ba64
chore: interior-mut shouldn't fail with this pr
Stevengre Nov 4, 2025
e319042
chore: add comments
Stevengre Nov 4, 2025
96dc111
feat: support ZSTs
Stevengre Nov 4, 2025
e4b482c
chore: interior-mut3 should pass
Stevengre Nov 5, 2025
430dd93
fix: adjust stack projection writes
Stevengre Nov 5, 2025
6cb7e3f
feat: support cast from bytes to int
Stevengre Nov 5, 2025
e5f30b7
feat: support ref borrow (need to optimize)
Stevengre Nov 5, 2025
0a78bae
feat: support cast from int to bytes
Stevengre Nov 5, 2025
d0c1793
restore stable-mir-json
Stevengre Nov 5, 2025
08389d0
chore: format
Stevengre Nov 5, 2025
2e1aeb1
feat: add #withPointerOffset to support projections' pointer offset
Stevengre Nov 5, 2025
1b24944
feat: enhance interior mutability handling in projections
Stevengre Nov 5, 2025
5ca54b5
refactor: remove unused NormalSym population logic in _functions
Stevengre Nov 5, 2025
4683341
feat: simplify borrow cell increment and decrement logic for interior…
Stevengre Nov 5, 2025
a8b3258
feat: add handling for pointer realignment across transparent wrapper…
Stevengre Nov 5, 2025
f1c3005
feat: initialize zero-sized locals for borrowing to ensure projection…
Stevengre Nov 5, 2025
d94197b
feat: streamline alignment rule for struct types in #alignOf function
Stevengre Nov 5, 2025
d45a24a
feat: update expected output for pointer cast length test and symboli…
Stevengre Nov 5, 2025
69a4efd
feat: add comment for pointer transmutation test and correctness check
Stevengre Nov 5, 2025
eb83742
feat: add static array checks for transmute operations in MIR execution
Stevengre Nov 5, 2025
b13b312
feat: refactor type identification for Ref and RefMut in type metadata
Stevengre Nov 5, 2025
d3b81e1
feat: update expected step count in crate2::test_crate1_with test
Stevengre Nov 5, 2025
716dc16
feat: refine drop semantics and enhance comments for clarity
Stevengre Nov 5, 2025
3450bc8
feat: enhance Drop terminator documentation and clarify borrow-aware …
Stevengre Nov 5, 2025
1efd5f7
feat: update expected step count in crate2::main.expected test
Stevengre Nov 5, 2025
cd57064
feat: enhance drop semantics to support general drops and improve bor…
Stevengre Nov 6, 2025
0a16989
feat: enhance borrow reference handling and clarify aggregate process…
Stevengre Nov 6, 2025
0b07a30
Update kmir/src/kmir/kdist/mir-semantics/kmir.md
Stevengre Nov 6, 2025
d57f4f3
Update kmir/src/kmir/kdist/mir-semantics/kmir.md
Stevengre Nov 6, 2025
541edd4
feat: update expected step count in crate2::test_crate1_with.expected
Stevengre Nov 6, 2025
193bef5
chore: update expected output
Stevengre Nov 6, 2025
8358db0
test: ensure interior mut refcell updates mint and account data
Stevengre Nov 6, 2025
3b3ef6a
docs(rt): Clarify zero sized type limitations
Stevengre Nov 6, 2025
9cc3eaf
moved to "jh/int-bytes-cast"
Stevengre Nov 6, 2025
8a77758
move to `jh/correct-offset`
Stevengre Nov 6, 2025
8e75511
moved to `jh/zero-sized`
Stevengre Nov 6, 2025
4f9fcd9
moved to `jh/interior-mut`
Stevengre Nov 6, 2025
83c924c
moved to `jh/zero-sized`
Stevengre Nov 6, 2025
54ceab5
chore: make ci fail faster
Stevengre Nov 7, 2025
00e2df2
chore: moved to jh/align-transparent-place
Stevengre Nov 7, 2025
55f9281
chore: moved to jh/pointer2int
Stevengre Nov 7, 2025
5c6128e
chore: moved to jh/delete-doc
Stevengre Nov 7, 2025
61c8c69
chore: remove empty lines
Stevengre Nov 7, 2025
8cc88c4
chore: move to jh/align-transparent-place
Stevengre Nov 7, 2025
82392e7
chore: move to jh/align-transparent-place
Stevengre Nov 7, 2025
cca1452
chore: move to jh/align-transparent-place
Stevengre Nov 7, 2025
76a081e
chore: move to jh/zero-sized-decode
Stevengre Nov 7, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
121 changes: 121 additions & 0 deletions kmir/src/tests/integration/data/prove-rs/refcell.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,121 @@
//! Minimal dual-AccountInfo harness for MIR semantics tests.

use std::cell::{Ref, RefCell, RefMut};

trait MiniPack: Copy {
const LEN: usize;
fn pack_into_slice(self, dst: &mut [u8]);
fn unpack_unchecked(src: &[u8]) -> Self
where
Self: Sized;
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct MiniMint {
decimals: u8,
supply: u64,
}

impl MiniPack for MiniMint {
const LEN: usize = 9;

fn pack_into_slice(self, dst: &mut [u8]) {
assert_eq!(dst.len(), Self::LEN);
dst[0] = self.decimals;
dst[1..].copy_from_slice(&self.supply.to_le_bytes());
}

fn unpack_unchecked(src: &[u8]) -> Self {
let mut supply = [0_u8; 8];
supply.copy_from_slice(&src[1..]);
Self {
decimals: src[0],
supply: u64::from_le_bytes(supply),
}
}
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
struct MiniTokenAccount {
owner: [u8; 8],
amount: u64,
status: u8,
}

impl MiniPack for MiniTokenAccount {
const LEN: usize = 17;

fn pack_into_slice(self, dst: &mut [u8]) {
assert_eq!(dst.len(), Self::LEN);
dst[0..8].copy_from_slice(&self.owner);
dst[8..16].copy_from_slice(&self.amount.to_le_bytes());
dst[16] = self.status;
}

fn unpack_unchecked(src: &[u8]) -> Self {
let mut owner = [0_u8; 8];
owner.copy_from_slice(&src[0..8]);
let mut amount = [0_u8; 8];
amount.copy_from_slice(&src[8..16]);
Self {
owner,
amount: u64::from_le_bytes(amount),
status: src[16],
}
}
}

pub struct AccountInfo<'a> {
data: RefCell<&'a mut [u8]>,
}

impl<'a> AccountInfo<'a> {
pub fn new(data: &'a mut [u8]) -> Self {
Self {
data: RefCell::new(data),
}
}

pub fn borrow_data(&self) -> Ref<'_, [u8]> {
Ref::map(self.data.borrow(), |slice| &**slice)
}

pub fn borrow_mut_data(&self) -> RefMut<'_, [u8]> {
RefMut::map(self.data.borrow_mut(), |slice| &mut **slice)
}
}

#[no_mangle]
Copy link
Collaborator

Choose a reason for hiding this comment

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

What is the reason for adding no mangle? Is that necessary?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.

pub fn dual_account_demo(account_info: &AccountInfo, mint_info: &AccountInfo) -> bool {
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);
Copy link
Collaborator

Choose a reason for hiding this comment

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

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?

Copy link
Contributor Author

Choose a reason for hiding this comment

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

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.


true
}

fn main() {
let mut account_bytes = [0_u8; MiniTokenAccount::LEN];
let mut mint_bytes = [0_u8; MiniMint::LEN];
let account = AccountInfo::new(&mut account_bytes);
let mint = AccountInfo::new(&mut mint_bytes);
let result = dual_account_demo(&account, &mint);
assert!(result);
}