Repository navigation

Challenge 26: verify Rc/Weak safety in alloc::rc with Kani - #582

Open

v3risec wants to merge 33 commits into

model-checking:mainfrom

v3risec:challenge-26-rc

Open

Challenge 26: verify Rc/Weak safety in alloc::rc with Kani#582
v3risec wants to merge 33 commits into
model-checking:mainfrom
v3risec:challenge-26-rc

Commits on Oct 21, 2026
- alloc::rc: add Kani contracts and proofs for Challenge 26
  v3risec
  committed
  1efe287
- add core::mem::forget(..) to fix verification failures; refactor some harnesses with rust macro
  
  MinghuaWang
  authored and
  v3risec
  committed
  a594e23
- refactor some harnesses with macro
  
  MinghuaWang
  authored and
  v3risec
  committed
  2357bc9
- refactor rc verification harnesses with macros; fix verification failures
  v3risec
  committed
  c6e9888
- update rc verification harnesses with macros; fix verification failures
  v3risec
  committed
  61c5a3d
- fix rc Kani harness review issues
  v3risec
  committed
  05b4525
- Add Rc raw allocator harnesses and refine assume_init slice harness
  v3risec
  committed
  3ece82d
- refine rc new harness
  v3risec
  committed
  42f6600
- add bound for macOS env; restruct some harnesses
  v3risec
  committed
  8e623da
- refactor harnesses to fix CI failures
  v3risec
  committed
  8e3dc14
- alloc: address Rc verification review feedback
  v3risec
  committed
  5c914f6
- alloc: bound Rc get_mut slice harnesses
  v3risec
  committed
  df22fc8
- alloc: bound Weak from_raw_in slice harnesses to reduce CI resource usage
  v3risec
  committed
  42e55f3
- alloc: bound Rc harnesses to reduce CI resources, not a verification gap
  v3risec
  committed
  988b617
- Strengthen Rc contracts and Kani harnesses, and fix assume_init harnesses issues
  v3risec
  committed
  8c0b1ae
- add try_from verification method
  v3risec
  committed
  03ff356
- alloc: strengthen Rc Kani harnesses
  v3risec
  committed
  92c7d92
- alloc: verify remaining Rc slice construction paths
  v3risec
  committed
  4e2a32d
- alloc: add reachability witnesses to Rc contracts
  v3risec
  committed
  aec03f9
- Strengthen Rc/Weak Kani contracts and harnesses
  v3risec
  committed
  0dcb818
- fix align_of_val_raw error
  v3risec
  committed
  56ca0ba
- Address final review items for Challenge 26
  v3risec
  committed
  4309886
- Update Rc::into_array harness for Result return type
  v3risec
  committed
  786f3da
- lower bound to keep CI tractability
  v3risec
  committed
  6ce45e7
- Update Rc verification after upstream rebase
  v3risec
  committed
  8f799d2
- update lib.rs
  v3risec
  committed
  417ff95
- ci: rerun verification
  v3risec
  committed
  19a4012
Commits on Oct 22, 2026
- Adjust Rc harnesses for Kani validity-check limitations
  v3risec
  committed
  b6e77a3
- Merge branch 'main' into challenge-26-rc
  v3risec
  authored
  5c1ba45
Commits on Oct 23, 2026
- fix CI error
  v3risec
  committed
  8b09fb5
- ci: trigger CI rerun
  v3risec
  committed
  fa0abd4
Commits on Nov 10, 2026
- Merge branch 'main' into challenge-26-rc
  v3risec
  authored
  b23c5c0
- Restore Rc verification harnesses and overflow checks
  v3risec
  committed
  021bd3a

Commits

Commits on Oct 21, 2026

Commits on Oct 22, 2026

Commits on Oct 23, 2026

Commits on Nov 10, 2026