Proposal for new Kani API similar to `CPROVER_r_ok` and `CPROVER_w_ok`

[QinyuanWu]

Requested feature: Kani API to verify whether a segment in memory is valid for read or write, similar to CPROVER_r_ok and CPROVER_w_ok Use case: Writing function contracts that meet the safety requirement where the pointer must be valid for reads or writes of a certain number of bytes. std::ptr::copy is an example.

Link to relevant documentation (Rust reference, Nomicon, RFC): CPROVER memory primitives The current workaround is to cast the pointer to the size of the number of bytes that need to be checked and use ub_checks::can_dereference on the pointer. However, a specific API like CPROVER_r_ok and CPROVER_w_ok would be more accurate. Thank you! @Dhvani-Kapadia @zhassan-aws @celinval

[celinval]

Hi @QinyuanWu, just so I make sure I understand the request. Would you like an option that you can provide the size to be read or a function that only checks allocation status (or both)?

The can_dereference and can_write provide extra checks that CPROVER_r_ok doesn't provide, such as value validity, pointer alignment and memory initialization (if the feature is enabled). We're likely going to extend those APIs later to provide things such as aliasing checks.