Contracts & Harnesses for `non_null::sub` and `non_null::sub_ptr` and `non_null::offset_from`#93

Merged

zhassan-aws merged 37 commits intomodel-checking:mainfrom

danielhumanmod:jimmy_develop

Nov 27, 2024

Commits on Sep 12, 2024

added contract and proof for new_unchecked

OwO
authored and
OwO
committed
add use safety

OwO
authored and
OwO
committed
verification result

OwO
authored and
OwO
committed

Commits on Sep 13, 2024

make harness function name unique
QinyuanWu
committed

Commits on Sep 14, 2024

add new_unchcked result and remove the old one
QinyuanWu
committed

Commits on Sep 18, 2024

Commits on Sep 24, 2024

complete the sub function proof
Jimmycreative
committed

Commits on Sep 26, 2024

Commits on Oct 9, 2024

fix some issue
Jimmycreative
committed

Commits on Oct 22, 2024

the SIZE should also be equal
Jimmycreative
committed

Commits on Nov 14, 2024

fix the proof based on the comments
Jimmycreative
committed

Commits on Nov 22, 2024

refine the code based on the suggestions

Jimmycreative
and
Carolyn Zech
authored
refine the code based on the suggestions

Jimmycreative
and
Carolyn Zech
authored
remove the old comment

Jimmycreative
and
Carolyn Zech
authored