b1d261a295
fix: fix an error in requires of dealloc
2025-10-29 13:49:11 +08:00
e74d1c7775
fix: fix the error of core imports
2025-10-17 17:09:04 +08:00
0ac03fd258
fix: add missing core imports to resolve compile errors
2025-10-17 16:54:55 +08:00
7e49167a73
style: change the dependency of vstd
2025-10-16 22:12:02 +08:00
7880e0762d
style: change package name to verified-memory-allocator
2025-10-16 22:03:07 +08:00
99feb5c9af
style: change edition 2024 to 2021
2025-10-16 21:58:23 +08:00
b0c0ecf9f8
perf: update v3_impl to improve performance and add some tests
2025-10-16 21:23:10 +08:00
5de1ebac15
refactor: refactor the project structure, add the original implementation code, and test performance
...
Refactor the project structure, add the original implementation code, and use the Criterion library
to compare the performance between the “original implementation” and the “Verus implementation”.
2025-10-05 18:46:16 +08:00
8b3d9f5269
style: restructure the project to remain consistent with the original bitmap-allocator
2025-09-28 17:09:39 +08:00
0eb74fc673
Update README.md
2025-09-26 20:01:23 +08:00
8eef3f1764
docs: change the fixture of BitAlloc_struct.png
2025-09-26 19:48:50 +08:00
8fa8d250ad
docs: add some images
2025-09-26 19:16:18 +08:00
df4ad86b93
feat: completion of the initial proof(v0) for the memory allocator
2025-09-24 15:41:53 +08:00
b96424f326
feat: add a function "set_range_to" in trait "BitAlloc"
...
The function "set_range_to" is called by "insert()" and "remove()", and the proof has been
simplified.
2025-09-21 16:57:35 +08:00
4fdd379212
feat: completed the function of remove
2025-09-21 14:35:17 +08:00
e959a32aa3
feat: completed the function of insert, but have 2 assume
2025-09-19 08:58:35 +08:00
90755fe0fd
Create LICENSE
2025-09-07 15:38:23 +08:00
a0dfcb477b
feat: completed the function of dealloc and change the struct BitAllocCascade16
...
completed the function of dealloc and change the struct BitAllocCascade16<T: BitAllocView> to
BitAllocCascade16<T>
2025-09-05 19:20:11 +08:00
23eacb0c28
feat(bitalloccascade16): implemented the alloc function for the 16-level tree structure
2025-09-04 14:17:31 +08:00
498eb9f7ee
Rewrite `find_map` as a `while` loop.
2025-08-04 19:45:22 +08:00
787aa60cb6
complet the proof of seq_index < 16
2025-08-04 11:32:52 +08:00
56634a0afc
Split the "BitAlloc" trait into modified values "BitAlloc" and unmodified values "BitAllocView"
2025-08-03 23:34:42 +08:00
4ffc3be654
add the feature of trait
2025-07-28 21:39:21 +08:00
0f629fa692
Fixed the previous error in the proof of find_contiguous
2025-07-20 16:02:12 +08:00
5694523a62
Tidy up the bitmap_vec.rs file, add comments
2025-07-14 15:28:47 +08:00
4c24d5fec6
The proof of bitalloc16 has been completed.
2025-06-30 23:49:15 +08:00
01341e7680
change the find_contiguous
2025-06-25 19:15:52 +08:00
5f9ee1819f
define the find_contiguous
2025-06-20 19:24:56 +08:00
cd08efc579
complete the insert and remove
2025-06-19 19:15:00 +08:00
c489314c55
complete the next
2025-06-17 20:26:18 +08:00
e7a3894c5d
chang the next func
2025-06-14 17:01:16 +08:00
f6f42d6a97
complete the verification of the alloc of bitalloc16
2025-06-12 18:42:32 +08:00
4e731edc94
init FrameAllocatorState and some spec of alloc
2025-05-12 08:52:38 +08:00
d995f6bc85
Initial commit
2025-05-11 16:09:24 +08:00
LiuJun5817
LiuJun