Add implementation of padding_needed_for

[ezrosent]

Description says it all. The implementation has detailed comments. Happy to edit commit messages as needed.

[jswrenn]

Re-run the UI tests with:

TRYBUILD=overwrite ./cargo.sh +all test -p zerocopy --features derive
TRYBUILD=overwrite ./cargo.sh +all test -p zerocopy-derive

[jswrenn]

Happy to say that the new implementation passes kani, with some slight modifications to the kani harness:

    #[kani::proof]
    fn prove_padding_needed_for() {
        fn model_impl(len: usize, align: NonZeroUsize) -> usize {
            let padded = len.next_multiple_of(align.get());
            let padding = padded - len;
            padding
        }

        // Generate a valid alignment.
        let align: NonZeroUsize = {
            let align: NonZeroUsize = kani::any();
            kani::assume(align.get().is_power_of_two());
            kani::assume(align.get() < 1 << 29);
            align
        };

        // Generate a valid length.
        let len: usize = {
            let len: usize = kani::any();
            kani::assume(len <= isize::MAX as usize);
            len
        };

        // Assert that the optimized and model implementations behave
        // identically.
        let expected = model_impl(len, align);
        let actual = padding_needed_for(len, align);
        assert_eq!(expected, actual, "padding_needed_for({len}, {align})");

        // Basic correctness checks.
        let padded_len = actual + len;
        assert_eq!(padded_len % align, 0);
        assert!(padded_len / align >= len / align);
    }

You can verify this by running:

cargo kani --harness prove_padding_needed_for --output-format terse

The one big thing that needs to be done before merging is to shift over the callsites to padding_needed_for. You ought to be able to do this by deleting the vendored implementation, and replacing all instances of util::core_layout::padding_needed_for with util::padding_needed_for (that should get you 90% of the way there).

[ezrosent]

Looks like everything passes now; thanks for adding the kani test!

Discussed offline