Skip to main content

spacewasm/
memory.rs

1use crate::Rc;
2use crate::{AllocError, MemType};
3use core::alloc::Layout;
4use core::fmt::{Debug, Formatter};
5use core::ptr::NonNull;
6use core::slice;
7
8/// An allocator for allocating Wasm pages
9pub trait WasmMemoryAllocator {
10    /// Allocate a new memory region for linear memory
11    fn allocate(&self, layout: Layout) -> Result<NonNull<u8>, AllocError>;
12
13    /// Reallocate a memory region, moving data if needed.
14    ///
15    /// On success, returns a pointer to a block of `layout` whose leading
16    /// `old_layout.size()` bytes hold the previous contents; the old allocation
17    /// (`ptr`/`old_layout`) has been consumed and must not be used again.
18    ///
19    /// # Failure ownership contract
20    ///
21    /// On `Err`, the implementation MUST leave the original allocation
22    /// (`ptr` with `old_layout`) valid, unmoved, and still owned by the caller.
23    fn reallocate(
24        &self,
25        ptr: NonNull<u8>,
26        old_layout: Layout,
27        layout: Layout,
28    ) -> Result<NonNull<u8>, AllocError>;
29
30    /// Deallocate memory that has been allocated
31    fn deallocate(&self, ptr: NonNull<u8>, layout: Layout);
32}
33
34impl<T: WasmMemoryAllocator> Rc<T> {
35    pub fn into_wasm_memory_allocator(self) -> Rc<dyn WasmMemoryAllocator>
36    where
37        T: WasmMemoryAllocator + 'static,
38    {
39        unsafe { self.into_dyn(|x| x as &dyn WasmMemoryAllocator) }
40    }
41}
42
43/// A WebAssembly linear memory
44///
45/// Linear memory implements inner mutability so it is not thread-safe.
46/// `Memory` holds a raw pointer, so it is automatically `!Send + !Sync`.
47///
48/// Needs to have inner mutability because multiple modules can point
49/// to it (via imports) and we use `Rc<Memory>` for reference counting these ownerships.
50///
51/// # Aliasing model
52///
53/// The `store_*` mutators take `&self`, so the borrow checker will not stop you
54/// from writing these bytes while a shared reference into them is alive. Drop
55/// any [`Memory::load`] / [`Memory::get_slice`] slice before any write —
56/// `store_*`, [`Memory::grow`] (which may reallocate), a host callback, or guest
57/// re-entry. Holding one across a write is UB under Stacked Borrows.
58/// [`Memory::as_shared_cells`] is the one aliasing-tolerant accessor.
59pub struct Memory {
60    ptr: *mut u8,
61    size: usize,
62    ty: MemType,
63    allocator: Option<Rc<dyn WasmMemoryAllocator>>,
64}
65
66impl Debug for Memory {
67    fn fmt(&self, f: &mut Formatter<'_>) -> core::fmt::Result {
68        f.debug_struct("Memory").finish()
69    }
70}
71
72#[derive(Debug, Clone, PartialEq, Eq)]
73pub enum MemoryError {
74    OutOfBounds,
75    OutOfMemory,
76    AllocationFailed,
77    PageTooSmall,
78}
79
80impl From<AllocError> for MemoryError {
81    fn from(e: AllocError) -> MemoryError {
82        match e {
83            AllocError::AllocationFailed => MemoryError::AllocationFailed,
84            AllocError::OutOfMemory => MemoryError::OutOfMemory,
85            AllocError::PageTooSmall => MemoryError::PageTooSmall,
86        }
87    }
88}
89
90impl Default for Memory {
91    fn default() -> Self {
92        Memory::zero()
93    }
94}
95
96impl Memory {
97    pub fn zero() -> Memory {
98        Memory {
99            ptr: core::ptr::null_mut(),
100            size: 0,
101            ty: MemType::zero(),
102            allocator: None,
103        }
104    }
105
106    pub fn new(ty: MemType, allocator: Rc<dyn WasmMemoryAllocator>) -> Result<Memory, AllocError> {
107        let size = if let Some(size) = (ty.min() as u64).checked_mul(ty.page_size() as u64) {
108            if size > usize::MAX as u64 {
109                // Make sure this platform can actually do this allocation
110                return Err(AllocError::AllocationFailed);
111            } else {
112                size as usize
113            }
114        } else {
115            return Err(AllocError::AllocationFailed);
116        };
117
118        let ptr = if size == 0 {
119            core::ptr::null_mut()
120        } else {
121            let ptr = allocator
122                .allocate(
123                    Layout::from_size_align(size, ty.page_alignment())
124                        .map_err(|_| AllocError::AllocationFailed)?,
125                )?
126                .as_ptr();
127
128            // Clear the pages
129            unsafe {
130                ptr.write_bytes(0, size);
131            }
132            ptr
133        };
134
135        Ok(Memory {
136            ptr,
137            size,
138            ty,
139            allocator: Some(allocator),
140        })
141    }
142}
143
144impl Memory {
145    #[inline]
146    fn check_in_bounds(&self, addr: usize, size: usize) -> Result<(), MemoryError> {
147        if size > self.size || addr > self.size - size {
148            Err(MemoryError::OutOfBounds)
149        } else {
150            Ok(())
151        }
152    }
153
154    /// Resolve a guest memory access `base + offset` to a byte address.
155    ///
156    /// The sum is evaluated in `u64` and narrowed back to `usize`, so it can
157    /// never wrap on 32-bit targets, where `usize` is 32-bit and `base + offset`
158    /// may exceed `u32::MAX`. An address that does not fit `usize` is rejected as
159    /// out of bounds rather than aliasing a valid cell. The resulting address is
160    /// still bounds-checked against the memory size by the individual load/store
161    /// operations.
162    #[inline]
163    pub fn effective_address(base: u32, offset: u32) -> Result<usize, MemoryError> {
164        usize::try_from(base as u64 + offset as u64).map_err(|_| MemoryError::OutOfBounds)
165    }
166
167    pub fn store_u8(&self, addr: usize, i: u8) -> Result<(), MemoryError> {
168        self.check_in_bounds(addr, 1)?;
169        unsafe {
170            self.ptr.add(addr).write(i);
171        }
172        Ok(())
173    }
174
175    pub fn store_u16(&self, addr: usize, i: u16) -> Result<(), MemoryError> {
176        self.check_in_bounds(addr, 2)?;
177        unsafe {
178            self.ptr.add(addr).cast::<u16>().write_unaligned(i.to_le());
179        }
180        Ok(())
181    }
182
183    pub fn store_u32(&self, addr: usize, i: u32) -> Result<(), MemoryError> {
184        self.check_in_bounds(addr, 4)?;
185        unsafe {
186            self.ptr.add(addr).cast::<u32>().write_unaligned(i.to_le());
187        }
188        Ok(())
189    }
190
191    pub fn store_u64(&self, addr: usize, i: u64) -> Result<(), MemoryError> {
192        self.check_in_bounds(addr, 8)?;
193        unsafe {
194            self.ptr.add(addr).cast::<u64>().write_unaligned(i.to_le());
195        }
196        Ok(())
197    }
198
199    pub fn store(&self, addr: usize, data: &[u8]) -> Result<(), MemoryError> {
200        self.check_in_bounds(addr, data.len())?;
201        if data.is_empty() {
202            return Ok(());
203        }
204
205        unsafe {
206            data.as_ptr().copy_to(self.ptr.add(addr), data.len());
207        }
208        Ok(())
209    }
210
211    pub fn load_u8(&self, addr: usize) -> Result<u8, MemoryError> {
212        self.check_in_bounds(addr, 1)?;
213        unsafe { Ok(self.ptr.add(addr).read()) }
214    }
215
216    pub fn load_u16(&self, addr: usize) -> Result<u16, MemoryError> {
217        self.check_in_bounds(addr, 2)?;
218        unsafe {
219            Ok(u16::from_le(
220                self.ptr.add(addr).cast::<u16>().read_unaligned(),
221            ))
222        }
223    }
224
225    pub fn load_u32(&self, addr: usize) -> Result<u32, MemoryError> {
226        self.check_in_bounds(addr, 4)?;
227        unsafe {
228            Ok(u32::from_le(
229                self.ptr.add(addr).cast::<u32>().read_unaligned(),
230            ))
231        }
232    }
233
234    pub fn load_u64(&self, addr: usize) -> Result<u64, MemoryError> {
235        self.check_in_bounds(addr, 8)?;
236        unsafe {
237            Ok(u64::from_le(
238                self.ptr.add(addr).cast::<u64>().read_unaligned(),
239            ))
240        }
241    }
242
243    pub fn load(&self, addr: usize, len: usize) -> Result<&[u8], MemoryError> {
244        self.check_in_bounds(addr, len)?;
245        if len == 0 {
246            return Ok(&[]);
247        }
248        Ok(unsafe { core::slice::from_raw_parts(self.ptr.add(addr), len) })
249    }
250
251    /// Grow the memory by n pages
252    /// If the memory growth succeeds, return the old number of pages
253    pub fn grow(&mut self, n: u32) -> Result<u32, MemoryError> {
254        let old_pages = self.size();
255        let total_pages = old_pages.checked_add(n).ok_or(MemoryError::OutOfMemory)?;
256
257        if !self.ty.can_hold(total_pages) {
258            return Err(MemoryError::OutOfMemory);
259        }
260
261        let allocator = self.allocator.as_ref().ok_or(MemoryError::OutOfMemory)?;
262        if n == 0 {
263            return Ok(old_pages);
264        }
265
266        let old_size = self.size;
267        let new_size = usize::try_from(u64::from(total_pages) * self.ty.page_size() as u64)
268            .map_err(|_| MemoryError::OutOfMemory)?;
269        let new_layout = Layout::from_size_align(new_size, self.ty.page_alignment())
270            .map_err(|_| MemoryError::AllocationFailed)?;
271
272        let ptr = if old_size == 0 {
273            allocator.allocate(new_layout)?
274        } else {
275            allocator.reallocate(
276                NonNull::new(self.ptr).ok_or(MemoryError::OutOfMemory)?,
277                Layout::from_size_align(old_size, self.ty.page_alignment())
278                    .map_err(|_| MemoryError::AllocationFailed)?,
279                new_layout,
280            )?
281        };
282
283        // Clear the new memory before committing the larger size.
284        unsafe {
285            ptr.as_ptr()
286                .add(old_size)
287                .write_bytes(0, new_size - old_size);
288        }
289
290        self.ptr = ptr.as_ptr();
291        self.size = new_size;
292
293        Ok(old_pages)
294    }
295
296    pub fn mem_type(&self) -> MemType {
297        self.ty
298    }
299
300    pub fn size(&self) -> u32 {
301        (self.size / self.ty.page_size()) as u32
302    }
303
304    /// Returns whether this is the absent-memory sentinel created by [`Memory::zero`].
305    pub fn is_zero(&self) -> bool {
306        self.ptr.is_null() && self.allocator.is_none()
307    }
308
309    pub fn get_slice(&self) -> &[u8] {
310        if self.ptr.is_null() {
311            &[]
312        } else {
313            unsafe { slice::from_raw_parts(self.ptr, self.size) }
314        }
315    }
316
317    /// Expose linear memory as `&[UnsafeCell<u8>]`.
318    ///
319    /// Unlike [`get_slice`], this view stays valid across writes, which is what
320    /// makes it usable as a `wiggle` `GuestMemory::Shared` backing store. Still
321    /// invalidated by [`Memory::grow`]. Empty for the [`Memory::zero`] sentinel.
322    ///
323    /// [`get_slice`]: Memory::get_slice
324    pub fn as_shared_cells(&self) -> &[core::cell::UnsafeCell<u8>] {
325        if self.ptr.is_null() {
326            &[]
327        } else {
328            unsafe {
329                core::slice::from_raw_parts(
330                    self.ptr as *const core::cell::UnsafeCell<u8>,
331                    self.size,
332                )
333            }
334        }
335    }
336}
337
338impl Drop for Memory {
339    fn drop(&mut self) {
340        if !self.ptr.is_null() {
341            let allocator = self.allocator.take().unwrap();
342            allocator.deallocate(
343                NonNull::new(self.ptr).unwrap(),
344                Layout::from_size_align(self.size, self.ty.page_alignment()).unwrap(),
345            )
346        }
347    }
348}
349
350#[cfg(test)]
351mod tests {
352    use super::*;
353    use crate::MemPageSize;
354    extern crate std;
355
356    /// Test allocator backed by the system heap, mirroring the one used in
357    /// `interpreter_tests`.
358    struct TestAllocator;
359    impl WasmMemoryAllocator for TestAllocator {
360        fn allocate(&self, layout: Layout) -> Result<NonNull<u8>, AllocError> {
361            assert_ne!(layout.size(), 0);
362            unsafe { NonNull::new(std::alloc::alloc(layout)).ok_or(AllocError::AllocationFailed) }
363        }
364
365        fn reallocate(
366            &self,
367            ptr: NonNull<u8>,
368            old_layout: Layout,
369            layout: Layout,
370        ) -> Result<NonNull<u8>, AllocError> {
371            assert_ne!(old_layout.size(), 0);
372            assert_ne!(layout.size(), 0);
373            unsafe {
374                let new_ptr = std::alloc::realloc(ptr.as_ptr(), old_layout, layout.size());
375                NonNull::new(new_ptr).ok_or(AllocError::AllocationFailed)
376            }
377        }
378
379        fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
380            assert_ne!(layout.size(), 0);
381            unsafe { std::alloc::dealloc(ptr.as_ptr(), layout) }
382        }
383    }
384
385    fn allocator() -> Rc<dyn WasmMemoryAllocator> {
386        Rc::new(TestAllocator).unwrap().into_wasm_memory_allocator()
387    }
388
389    fn mem_type(min: u32, max: Option<u32>) -> MemType {
390        MemType {
391            initial_pages: min,
392            max_pages: max,
393            page_size: MemPageSize::_65536,
394        }
395    }
396
397    #[test]
398    fn zero_memory_is_zero() {
399        let mem = Memory::zero();
400        assert!(mem.is_zero());
401        assert_eq!(mem.size(), 0);
402    }
403
404    #[test]
405    fn new_allocates_and_reports_size() {
406        let mem = Memory::new(mem_type(2, Some(4)), allocator()).unwrap();
407        assert!(!mem.is_zero());
408        assert_eq!(mem.size(), 2);
409        assert_eq!(mem.mem_type().min(), 2);
410        // The freshly allocated pages are zeroed.
411        assert!(mem.get_slice().iter().all(|&b| b == 0));
412        assert_eq!(mem.get_slice().len(), 2 * MemPageSize::_65536.size());
413    }
414
415    #[test]
416    fn zero_page_memory_allocates_lazily() {
417        let mut mem = Memory::new(mem_type(0, None), allocator()).unwrap();
418
419        assert!(!mem.is_zero());
420        assert_eq!(mem.size(), 0);
421        assert!(mem.get_slice().is_empty());
422        assert_eq!(mem.load(0, 0), Ok(&[][..]));
423        assert_eq!(mem.store(0, &[]), Ok(()));
424        assert_eq!(mem.load(1, 0), Err(MemoryError::OutOfBounds));
425        assert_eq!(mem.store(1, &[]), Err(MemoryError::OutOfBounds));
426
427        assert_eq!(mem.grow(0), Ok(0));
428        assert_eq!(mem.grow(1), Ok(0));
429        assert_eq!(mem.size(), 1);
430        assert_eq!(mem.grow(0), Ok(1));
431        assert_eq!(mem.get_slice().len(), MemPageSize::_65536.size());
432        assert!(mem.get_slice().iter().all(|&b| b == 0));
433        assert_eq!(mem.load(0, 1), Ok(&[0][..]));
434        assert_eq!(mem.store(0, &[0xA5]), Ok(()));
435        assert_eq!(mem.load(0, 1), Ok(&[0xA5][..]));
436    }
437
438    #[test]
439    fn stores_are_little_endian() {
440        // Wasm mandates little-endian memory regardless of host byte order.
441        // Assert the actual byte layout, which round-trip tests cannot catch.
442        let mem = Memory::new(mem_type(1, None), allocator()).unwrap();
443
444        mem.store_u16(0, 0x1122).unwrap();
445        assert_eq!(mem.load(0, 2).unwrap(), &[0x22, 0x11][..]);
446
447        mem.store_u32(8, 0x1122_3344).unwrap();
448        assert_eq!(mem.load(8, 4).unwrap(), &[0x44, 0x33, 0x22, 0x11][..]);
449
450        mem.store_u64(16, 0x1122_3344_5566_7788).unwrap();
451        assert_eq!(
452            mem.load(16, 8).unwrap(),
453            &[0x88, 0x77, 0x66, 0x55, 0x44, 0x33, 0x22, 0x11][..]
454        );
455    }
456
457    #[test]
458    fn loads_are_little_endian() {
459        // A little-endian byte pattern must decode to the expected value.
460        let mem = Memory::new(mem_type(1, None), allocator()).unwrap();
461
462        mem.store(0, &[0x22, 0x11]).unwrap();
463        assert_eq!(mem.load_u16(0).unwrap(), 0x1122);
464
465        mem.store(8, &[0x44, 0x33, 0x22, 0x11]).unwrap();
466        assert_eq!(mem.load_u32(8).unwrap(), 0x1122_3344);
467
468        mem.store(16, &[0x88, 0x77, 0x66, 0x55, 0x44, 0x33, 0x22, 0x11])
469            .unwrap();
470        assert_eq!(mem.load_u64(16).unwrap(), 0x1122_3344_5566_7788);
471    }
472
473    #[test]
474    fn grow_extends_and_zeroes() {
475        let mut mem = Memory::new(mem_type(1, Some(4)), allocator()).unwrap();
476        // Write a marker into the first page.
477        mem.store_u32(0, 0xAABB_CCDD).unwrap();
478
479        let old_pages = mem.grow(2).unwrap();
480        assert_eq!(old_pages, 1);
481        assert_eq!(mem.size(), 3);
482
483        // Existing data survives the grow...
484        assert_eq!(mem.load_u32(0).unwrap(), 0xAABB_CCDD);
485        // ...and the newly added region is zeroed.
486        let first_new_byte = MemPageSize::_65536.size();
487        assert_eq!(mem.load_u8(first_new_byte).unwrap(), 0);
488    }
489
490    #[test]
491    fn grow_past_max_fails() {
492        let mut mem = Memory::new(mem_type(1, Some(2)), allocator()).unwrap();
493        // Growing to 3 pages exceeds the declared maximum of 2.
494        assert_eq!(mem.grow(2), Err(MemoryError::OutOfMemory));
495        // The memory is left untouched.
496        assert_eq!(mem.size(), 1);
497    }
498
499    #[test]
500    fn grow_overflow_page_count_fails() {
501        let mut mem = Memory::new(mem_type(1, None), allocator()).unwrap();
502        // `size() + n` overflows u32.
503        assert_eq!(mem.grow(u32::MAX), Err(MemoryError::OutOfMemory));
504    }
505
506    #[test]
507    fn grow_zero_memory_fails() {
508        // The absent-memory sentinel has no backing allocator.
509        let mut mem = Memory::zero();
510        assert_eq!(mem.grow(0), Err(MemoryError::OutOfMemory));
511        assert_eq!(mem.grow(1), Err(MemoryError::OutOfMemory));
512    }
513
514    #[test]
515    fn load_store_out_of_bounds() {
516        let mem = Memory::new(mem_type(1, None), allocator()).unwrap();
517        let size = MemPageSize::_65536.size();
518        assert_eq!(mem.load_u32(size - 3), Err(MemoryError::OutOfBounds));
519        assert_eq!(mem.store_u64(size - 4, 0), Err(MemoryError::OutOfBounds));
520        assert_eq!(mem.load(size - 1, 4), Err(MemoryError::OutOfBounds));
521    }
522
523    #[test]
524    fn effective_address_rejects_overflow_on_32bit() {
525        // On 64-bit `usize`, base+offset always fits; the sum is exact.
526        assert_eq!(Memory::effective_address(10, 20).unwrap(), 30);
527    }
528
529    #[test]
530    fn as_shared_cells_aliases_and_mutates() {
531        let mem = Memory::new(mem_type(1, None), allocator()).unwrap();
532
533        // The cell view covers exactly the linear memory bytes.
534        let cells = mem.as_shared_cells();
535        assert_eq!(cells.len(), mem.get_slice().len());
536
537        // A store is observable through the cell view...
538        mem.store_u8(3, 0x5A).unwrap();
539        assert_eq!(unsafe { *cells[3].get() }, 0x5A);
540
541        // ...and a write through a cell is observable through a load, which is
542        // the shared-but-mutable access wiggle relies on.
543        unsafe {
544            *cells[7].get() = 0xC3;
545        }
546        assert_eq!(mem.load_u8(7).unwrap(), 0xC3);
547    }
548
549    #[test]
550    fn as_shared_cells_zero_memory_is_empty() {
551        assert!(Memory::zero().as_shared_cells().is_empty());
552    }
553
554    #[test]
555    fn memory_error_from_alloc_error() {
556        assert_eq!(
557            MemoryError::from(AllocError::AllocationFailed),
558            MemoryError::AllocationFailed
559        );
560        assert_eq!(
561            MemoryError::from(AllocError::OutOfMemory),
562            MemoryError::OutOfMemory
563        );
564        assert_eq!(
565            MemoryError::from(AllocError::PageTooSmall),
566            MemoryError::PageTooSmall
567        );
568    }
569}
570
571#[cfg(kani)]
572mod kani_proofs {
573    use super::*;
574    use crate::Allocator;
575    use crate::MemPageSize;
576    extern crate std;
577
578    use crate::test_support::RustSystemAllocator;
579
580    #[kani::proof]
581    fn proof_store_load_correctness() {
582        let alloc = RustSystemAllocator;
583        let size = 64;
584
585        let ptr = unsafe {
586            alloc
587                .alloc(Layout::from_size_align(size, (MemPageSize::_65536).alignment()).unwrap())
588                .unwrap()
589        };
590        let mem = Memory {
591            ptr,
592            size,
593            ty: MemType::zero(),
594            allocator: None,
595        };
596
597        // Test all integer sizes with symbolic values and addresses
598        let addr: usize = kani::any();
599        kani::assume(addr <= size - 8); // Reserve space for largest type (u64)
600
601        // Test u8 store/load
602        let val_u8: u8 = kani::any();
603        mem.store_u8(addr, val_u8).unwrap();
604        assert_eq!(mem.load_u8(addr).unwrap(), val_u8, "u8 round-trip failed");
605
606        // Test u16 store/load
607        let val_u16: u16 = kani::any();
608        mem.store_u16(addr, val_u16).unwrap();
609        assert_eq!(
610            mem.load_u16(addr).unwrap(),
611            val_u16,
612            "u16 round-trip failed"
613        );
614
615        // Test u32 store/load
616        let val_u32: u32 = kani::any();
617        mem.store_u32(addr, val_u32).unwrap();
618        assert_eq!(
619            mem.load_u32(addr).unwrap(),
620            val_u32,
621            "u32 round-trip failed"
622        );
623
624        // Test u64 store/load
625        let val_u64: u64 = kani::any();
626        mem.store_u64(addr, val_u64).unwrap();
627        assert_eq!(
628            mem.load_u64(addr).unwrap(),
629            val_u64,
630            "u64 round-trip failed"
631        );
632
633        // Test out-of-bounds detection
634        assert!(
635            mem.store_u32(size - 2, 0).is_err(),
636            "Out-of-bounds store must fail"
637        );
638        assert!(
639            mem.store_u32(size, 0).is_err(),
640            "Store at boundary must fail"
641        );
642        assert!(
643            mem.load_u32(size - 2).is_err(),
644            "Out-of-bounds load must fail"
645        );
646        assert!(mem.load_u32(size).is_err(), "Load at boundary must fail");
647
648        // Test addresses that cause overflow in bounds check
649        let overflow_addr = usize::MAX - 1;
650        assert!(
651            mem.store_u32(overflow_addr, 0).is_err(),
652            "Overflow address must be rejected"
653        );
654        assert!(
655            mem.load_u32(overflow_addr).is_err(),
656            "Overflow address must be rejected"
657        );
658
659        // Verify safe addresses have lossless isize conversion
660        if addr <= isize::MAX as usize {
661            let offset = addr as isize;
662            assert!(offset >= 0, "Valid addr converts to non-negative offset");
663            assert!(offset as usize == addr, "isize conversion must be lossless");
664        }
665
666        // Prevent Drop from calling GlobalAllocator FFI
667        core::mem::forget(mem);
668        unsafe {
669            alloc.dealloc(
670                ptr,
671                Layout::from_size_align(size, (MemPageSize::_65536).alignment()).unwrap(),
672            )
673        };
674    }
675
676    #[kani::proof]
677    fn proof_byte_slice_operations() {
678        let alloc = RustSystemAllocator;
679        let size = 16;
680
681        let ptr = unsafe {
682            alloc
683                .alloc(Layout::from_size_align(size, (MemPageSize::_65536).alignment()).unwrap())
684                .unwrap()
685        };
686        let mem = Memory {
687            ptr,
688            size,
689            ty: MemType::zero(),
690            allocator: None,
691        };
692
693        // Test fixed-size byte slice (4 bytes) at symbolic address
694        let addr: usize = kani::any();
695        kani::assume(addr <= size - 4);
696
697        // Use symbolic 4-byte array
698        let data: [u8; 4] = kani::any();
699
700        // Store and load back
701        mem.store(addr, &data).unwrap();
702        let loaded = mem.load(addr, 4).unwrap();
703        assert_eq!(loaded, &data, "Byte slice round-trip failed");
704
705        // Test empty slice
706        mem.store(0, &[]).unwrap();
707        assert_eq!(mem.load(0, 0).unwrap().len(), 0, "Empty slice must work");
708
709        // Test out-of-bounds slice access
710        assert!(
711            mem.store(size - 2, &[1, 2, 3, 4]).is_err(),
712            "Out-of-bounds store must fail"
713        );
714        assert!(
715            mem.load(size - 2, 4).is_err(),
716            "Out-of-bounds load must fail"
717        );
718
719        // Prevent Drop from calling GlobalAllocator FFI
720        core::mem::forget(mem);
721        unsafe {
722            alloc.dealloc(
723                ptr,
724                Layout::from_size_align(size, (MemPageSize::_65536).alignment()).unwrap(),
725            )
726        };
727    }
728
729    /// The effective address is the exact sum of `base` and `offset`; it is
730    /// never silently wrapped modulo the pointer width.
731    #[kani::proof]
732    fn proof_effective_address_no_wrap() {
733        let base: u32 = kani::any();
734        let offset: u32 = kani::any();
735        let ea = Memory::effective_address(base, offset).unwrap();
736        assert_eq!(ea as u64, base as u64 + offset as u64);
737    }
738}