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
{{ message }}
Repository navigation
Challenge 25: Verify the safety of VecDeque functions #286
Solution PR: #681 (Kani; unbounded, symbolic ring layouts, contracts on all 13 unsafe functions, harnesses on all 30 safe abstractions; labelled Accepted Solution pending committee items). The open item is the "generic type T (no monomorphization)" clause, which Kani cannot meet literally; the ruling request with a proposed ruling text is here: #681 (comment).
Activity
vrindisbacher commentedon May 8, 2025
Hey there - following the book link gives me a 404. Is this still a challenge?
tautschnig commentedon May 9, 2025
It will become one, we just haven’t yet received approval from the rewards committee on #269.
Challenge 25: Verify safety of VecDeque
Challenge 25: Verify safety of VecDeque
Challenge 25: Verify safety of VecDeque
jrey8343 commentedon Sep 13, 2026
Solution PR: #681 (Kani; unbounded, symbolic ring layouts, contracts on all 13 unsafe functions, harnesses on all 30 safe abstractions; labelled Accepted Solution pending committee items). The open item is the "generic type
T(no monomorphization)" clause, which Kani cannot meet literally; the ruling request with a proposed ruling text is here: #681 (comment).