Challenge 26: Verify reference-counted Cell implementation

[AlexLB99]

#367

Runbook Link

https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html

[mohammad-shahabadi]

Hi all!
I’m interested in working on this challenge and would like to understand what has been done so far.
@ShoyuVanilla, are you actively working on this, or is there an opportunity for me to contribute?

[ShoyuVanilla]

I've been working on this and waiting for the kani version here to be updated up to model-checking/kani#4427 to write down remaining contracts, though I have no rights to block other people working on this 😅

[patricklam]

Thanks! We certainly don't want to duplicate any work that you have done / are ready to do. Are there any bits of this that you would want to cooperate on?

[ShoyuVanilla]

Umm I have written most contracts and just waiting for my kani PR mentioned above to write contracts for remaining two functions in "All the following pub unsafe functions must be annotated with safety contracts and the contracts have been verified:" part. For "These (not necessarily public) functions contain unsafe code in their bodies but are not themselves marked unsafe. At least 75% of these should be proven unconditionally safe, or safety contracts should be added." part, I have done to just meet the minimum requirement but cannot list what I have done exactly as they are in my home machine and I'm at work right now

[patricklam]

Sounds good. For getting practice, maybe Mohammad can look at the remaining ones, though I think that if you have done enough to collect the bounty, you should do so. We'll find some other challenge or propose another one. Could you share the list once you're at home?

[ShoyuVanilla]

Okay, I will

[patricklam]

Just a reminder... thanks.