One valid approach would be checking that the verification holds for all instantiations of (usize, isize) as (u16, i16), (u32, i32), (u64, i64), and (once [iu]usize supports it, since the integer types have landed) (u128, i128).
This potentially multiplies verification runtime by three, but as this only applies to functions which currently cannot be verified (those which use usize or isize) this seems relatively minor.
More concretely:
- If
S or Q contains values of type usize or isize, generate a list of (S, Q)_{i6,32,64} pairs, and calculate the corresponding weakest postcondition for each
- If neither contains such values, simply generate a single weakest postcondition (as now)
- If
P contains values of type usize or isize and multiple weakest postconditions were generated, generate a list of P_{16,32,64}, and prove that for all X in {16, 32, 64}, P_X -> WP_X
- If
P contains values of type usize or isize and only one weakest postcondition was generated, generate a list of P_{16,32,64} and show that for all X in {16, 32, 64}, P_X -> WP
- If
P does not contain values of type usize or isize, then show that all weakest postconditions are implied by the precondition.
One valid approach would be checking that the verification holds for all instantiations of
(usize, isize)as(u16, i16),(u32, i32),(u64, i64), and (once[iu]usizesupports it, since the integer types have landed)(u128, i128).This potentially multiplies verification runtime by three, but as this only applies to functions which currently cannot be verified (those which use
usizeorisize) this seems relatively minor.More concretely:
SorQcontains values of typeusizeorisize, generate a list of(S, Q)_{i6,32,64}pairs, and calculate the corresponding weakest postcondition for eachPcontains values of typeusizeorisizeand multiple weakest postconditions were generated, generate a list ofP_{16,32,64}, and prove that for allXin{16, 32, 64},P_X -> WP_XPcontains values of typeusizeorisizeand only one weakest postcondition was generated, generate a list ofP_{16,32,64}and show that for allXin{16, 32, 64},P_X -> WPPdoes not contain values of typeusizeorisize, then show that all weakest postconditions are implied by the precondition.