Multiple data types for pointer manipulation proofs

[QinyuanWu]

For pointer manipulation functions(e.g. add, sub, offset), we discussed the proofs should cover the following data types:

• All integer types.
• At least one dyn Trait.
• At least one slice.
• For unit type.
• At least one composite type with multiple non-ZST fields.

Would it be better to write separate proofs for each data type(this would result in 10+ proofs for each function) or to combine them in one proof? Since there are many integer types, is it enough to use an i8 array to represent all integer types? Thank you! @zhassan-aws

[carolynzech]

I would recommend writing separate harnesses for each of the types. It's nice to have smaller harnesses so that you can more easily pinpoint issues if verification fails or if a harness is posing a performance bottleneck.
For the integer types question -- no, we want to verify all integer types, not just i8. I would suggest writing a declarative macro that generates a harness given an integer type as a parameter. That way, it will be easy for you to generate harnesses for multiple integer types (and it also saves on space). For now, I'd recommend getting i8 working, and then you can move on to the other integer types.

[celinval]

Hi @QinyuanWu, please let us know if you have any follow up question or if we can close this question. Thanks!