You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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?
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 😅
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?
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
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?
Activity
[-][Tracking Challenge] Challenge 26: Verify reference-counted Cell implementation[/-][+]Challenge 26: Verify reference-counted Cell implementation[/+]fix: Make kani attribute nameres work with generic args having `::` (#…
mohammad-shahabadi commentedon Nov 17, 2025
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 commentedon Nov 18, 2025
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 commentedon Nov 18, 2025
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 commentedon Nov 18, 2025
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 commentedon Nov 18, 2025
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 commentedon Nov 18, 2025
Okay, I will
patricklam commentedon Nov 24, 2025
Just a reminder... thanks.
Challenge 26: Verify safety of Rc functions