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 17: Verify the safety of slice functions #281
For align_to and align_to_mut, can we assume that the target type U is a SIMD type and the source type T is a SimdElement, since the main use case seems to be as_simd and as_simd_mut?
For align_to and align_to_mut, can we assume that the target type U is a SIMD type and the source type T is a SimdElement, since the main use case seems to be as_simd and as_simd_mut?
We should not constrain proofs by current usage, but it may be a reasonable starting point to cover those cases and then try to find ways to prove the general case.
Hi, I'm working on a Kani-based solution for this challenge and have a question about the "no monomorphization" requirement.
Kani fundamentally relies on monomorphization — #[kani::proof_for_contract] verifies a contract for a specific concrete type instantiation, not universally for all T. This is an architectural limitation of the CBMC backend (each monomorphized instance is a distinct function at the GOTO level).
Our current approach uses 4 representative types that cover all distinct memory layout categories:
() — ZST (size 0, align 1)
u8 — small primitive (size 1, align 1)
char — validity-constrained (size 4, align 4)
(char, u8) — compound with padding (size 5+, align 4)
The reasoning is that the unsafe pointer operations in these functions (ptr::copy, ptr.add, get_unchecked, set_len, etc.) depend only on size_of::<T>() and align_of::<T>(), not on T's identity. These 4 types exercise all distinct behaviors: ZST special-casing, different strides, alignment constraints, and padding.
Question for the committee: Does this representative-types approach satisfy the "no monomorphization" requirement for Kani-based solutions? Or is a tool with inherent generic reasoning (like VeriFast's separation logic) required?
I'm also exploring a VeriFast-based solution as an alternative, but wanted to clarify the acceptance criteria first. The only resolved challenge with this requirement (Ch19 RawVec) was solved with VeriFast, so I wanted to confirm whether Kani solutions are viable here.
It verifies all 37 functions listed in the challenge: the 10 unsafe functions
(safety contracts + proof_for_contract at concrete monomorphizations) and all 27
safe abstractions (proven free of undefined behavior), using the existing mod verify + kani::slice::any_slice_of_array pattern, with explicit #[kani::unwind] bounds on the looping abstractions.
A few honest coverage notes are in the PR description (bounded backing-array length; get_unchecked/get_disjoint_* preconditions expressed via kani::assume because the
bound is index-type-specific over a generic I; and rotate_left/rotate_right
verified over concrete (length, amount) configurations because a symbolic rotation
amount makes ptr_rotate intractable for CBMC). I'd be happy to iterate on any of these.
@jrey8343 I appreciate you laying this question out so clearly, it is the crux of the
challenge. For what it is worth, I have a complete Kani solution up in #603 (all
37 functions, CI green), and it takes a similar representative-types route to the
one you describe, so it may be a useful data point for the committee either way.
On the substance, I agree with your reasoning: the unsafe operations in these
functions (ptr::copy, ptr.add, get_unchecked, set_len, and so on) depend
on size_of::<T>() and align_of::<T>() rather than on T's identity, so a
small set of representative types exercises the distinct layout behaviors. #603
uses unit, u8, u16, u32, u64, and char (plus usize and range index
types, and const-generic chunk sizes). Notably, it does not include a
compound-with-padding element type, so your (char, u8) case is a genuinely good
addition that mine is missing.
I do want to be straight about the limit, because I do not think either of us
should tell the committee this settles the "no monomorphization" criterion: a proof_for_contract at concrete instantiations is still monomorphized, so it is
strong evidence for the size-and-align argument rather than a literal
universal-over-T proof. #603 is also bounded in two honest ways I wrote up in
the PR: the symbolic slice length ranges over a fixed backing-array size, and rotate_left / rotate_right are checked over concrete (length, amount)
configurations because a symbolic rotation amount makes ptr_rotate intractable
for CBMC. Those two are exactly where a separation-logic tool like VeriFast could
give something Kani cannot, so if you are pursuing that angle it would be great to
compare notes rather than duplicate effort. I'll defer to the committee on whether
the representative-types approach clears the bar here.
Following up on my question above (2026-03-15) about the "generic type T (no monomorphization)" clause, which is still unanswered and which the reviewer's 09-12/09-13 triage marks as the acceptance gate for every Kani submission to this challenge: I have consolidated it into one ruling request with a concrete proposed ruling text (per-type instantiation with a stated coverage argument, or tool-level polymorphism only), posted on the Ch25 PR because that submission is the furthest along: #681 (comment). The same ruling governs this challenge; please answer there so there is one thread.
Activity
Lysxia commentedon May 19, 2025
For
align_toandalign_to_mut, can we assume that the target typeUis aSIMDtype and the source typeTis aSimdElement, since the main use case seems to beas_simdandas_simd_mut?tautschnig commentedon May 19, 2025
We should not constrain proofs by current usage, but it may be a reasonable starting point to cover those cases and then try to find ways to prove the general case.
jrey8343 commentedon Mar 15, 2026
Hi, I'm working on a Kani-based solution for this challenge and have a question about the "no monomorphization" requirement.
Kani fundamentally relies on monomorphization —
#[kani::proof_for_contract]verifies a contract for a specific concrete type instantiation, not universally for allT. This is an architectural limitation of the CBMC backend (each monomorphized instance is a distinct function at the GOTO level).Our current approach uses 4 representative types that cover all distinct memory layout categories:
()— ZST (size 0, align 1)u8— small primitive (size 1, align 1)char— validity-constrained (size 4, align 4)(char, u8)— compound with padding (size 5+, align 4)The reasoning is that the unsafe pointer operations in these functions (
ptr::copy,ptr.add,get_unchecked,set_len, etc.) depend only onsize_of::<T>()andalign_of::<T>(), not onT's identity. These 4 types exercise all distinct behaviors: ZST special-casing, different strides, alignment constraints, and padding.Question for the committee: Does this representative-types approach satisfy the "no monomorphization" requirement for Kani-based solutions? Or is a tool with inherent generic reasoning (like VeriFast's separation logic) required?
I'm also exploring a VeriFast-based solution as an alternative, but wanted to clarify the acceptance criteria first. The only resolved challenge with this requirement (Ch19 RawVec) was solved with VeriFast, so I wanted to confirm whether Kani solutions are viable here.
Verify safety of slice functions (Challenge 17)
Verify safety of slice functions (Challenge 17)
Verify safety of slice functions (Challenge 17)
Challenge 17: Verify safety of Slice functions
MavenRain commentedon Jun 17, 2026
Claiming Challenge 17 (Verify the safety of
slicefunctions).PR: #603
It verifies all 37 functions listed in the challenge: the 10 unsafe functions
(safety contracts +
proof_for_contractat concrete monomorphizations) and all 27safe abstractions (proven free of undefined behavior), using the existing
mod verify+kani::slice::any_slice_of_arraypattern, with explicit#[kani::unwind]bounds on the looping abstractions.A few honest coverage notes are in the PR description (bounded backing-array length;
get_unchecked/get_disjoint_*preconditions expressed viakani::assumebecause thebound is index-type-specific over a generic
I; androtate_left/rotate_rightverified over concrete
(length, amount)configurations because a symbolic rotationamount makes
ptr_rotateintractable for CBMC). I'd be happy to iterate on any of these.MavenRain commentedon Jul 8, 2026
@jrey8343 I appreciate you laying this question out so clearly, it is the crux of the
challenge. For what it is worth, I have a complete Kani solution up in #603 (all
37 functions, CI green), and it takes a similar representative-types route to the
one you describe, so it may be a useful data point for the committee either way.
On the substance, I agree with your reasoning: the unsafe operations in these
functions (
ptr::copy,ptr.add,get_unchecked,set_len, and so on) dependon
size_of::<T>()andalign_of::<T>()rather than onT's identity, so asmall set of representative types exercises the distinct layout behaviors. #603
uses unit,
u8,u16,u32,u64, andchar(plususizeand range indextypes, and const-generic chunk sizes). Notably, it does not include a
compound-with-padding element type, so your
(char, u8)case is a genuinely goodaddition that mine is missing.
I do want to be straight about the limit, because I do not think either of us
should tell the committee this settles the "no monomorphization" criterion: a
proof_for_contractat concrete instantiations is still monomorphized, so it isstrong evidence for the size-and-align argument rather than a literal
universal-over-
Tproof. #603 is also bounded in two honest ways I wrote up inthe PR: the symbolic slice length ranges over a fixed backing-array size, and
rotate_left/rotate_rightare checked over concrete(length, amount)configurations because a symbolic rotation amount makes
ptr_rotateintractablefor CBMC. Those two are exactly where a separation-logic tool like VeriFast could
give something Kani cannot, so if you are pursuing that angle it would be great to
compare notes rather than duplicate effort. I'll defer to the committee on whether
the representative-types approach clears the bar here.
jrey8343 commentedon Sep 13, 2026
Following up on my question above (2026-03-15) about the "generic type
T(no monomorphization)" clause, which is still unanswered and which the reviewer's 09-12/09-13 triage marks as the acceptance gate for every Kani submission to this challenge: I have consolidated it into one ruling request with a concrete proposed ruling text (per-type instantiation with a stated coverage argument, or tool-level polymorphism only), posted on the Ch25 PR because that submission is the furthest along: #681 (comment). The same ruling governs this challenge; please answer there so there is one thread.