Frontend performance regression

[maximebuyse]

Here is a reproducer, using dependencies on crates hkdf and sha2:

use hkdf::Hkdf;


pub fn hkdf_to_slice(salt: &[u8], ikm: &[u8]) {
    let _ = Hkdf::<sha2::Sha256>::new(Some(salt), ikm);
}

The regression in performance seems to come from 9625d1a

[Nadrieril]

My guess would be that this is caused by all the extra trait resolution to be done for the newly-added pervasive MetaSized bounds. We already cache trait resolution, I'm not sure what we could do better there.

[W95Psp]

I agree @Nadrieril, that was my guess I well, and I think we can confirm that's the issue, with the following reproducer:

use typenum::{IsLess, UInt, UTerm, B1};

type I17 = UInt<I16, B1>;
type I16 = UInt<I15, B1>;
type I15 = UInt<I14, B1>;
type I14 = UInt<I13, B1>;
type I13 = UInt<I12, B1>;
type I12 = UInt<I11, B1>;
type I11 = UInt<I10, B1>;
type I10 = UInt<I9, B1>;
type I9 = UInt<I8, B1>;
type I8 = UInt<I7, B1>;
type I7 = UInt<I6, B1>;
type I6 = UInt<I5, B1>;
type I5 = UInt<I4, B1>;
type I4 = UInt<I3, B1>;
type I3 = UInt<I2, B1>;
type I2 = UInt<I1, B1>;
type I1 = UInt<I0, B1>;
type I0 = UTerm;

type I = I13;

fn _f<T: IsLess<I>>() {}

I measured time for the different sizes of type-level integers (from I0 to I17) I get (after the commit and before the commit):

Data is:

I0,0.38,before
I1,0.38,before
I2,0.38,before
I3,0.38,before
I4,0.38,before
I5,0.38,before
I6,0.38,before
I7,0.38,before
I8,0.40,before
I9,0.38,before
I10,0.40,before
I11,0.43,before
I12,0.51,before
I13,0.78,before
I14,1.56,before
I15,3.98,before
I16,10.89,before
I17,32.32,before
I0,1.01,after
I1,0.37,after
I2,0.37,after
I3,0.37,after
I4,0.37,after
I5,0.37,after
I6,0.37,after
I7,0.39,after
I8,0.46,after
I9,0.84,after
I10,2.60,after
I11,11.34,after
I12,57.65,after

Get the data:

for v in before after; do for i in $(seq 0 $(cat src/lib.rs | grep -Po "I\K[0-9]+" | sort -n | tail -n1)); do sd 'type I = I.*;' "type I = I$i;" src/lib.rs; TIME=$({ /usr/bin/time ./$v/bin/cargo-hax hax json --use-ids -o json-$v-$i.json 2>&1 } | tail -n1 | grep -Po "[0-9,]* real" | grep -Po "[0-9,]*" | sd ',' '.'); echo "I$i,$TIME,$v"; done; done

[W95Psp]

Do you use or plan to use any size-related trait information, @Nadrieril?

[Nadrieril]

Thanks for the quantitative analysis, that's super helpful!

I need it because Charon aims to be semantically precise and these traits are how we can track a type's size. We could easily add an option to filter out the Sized/MetaSized clauses in traits::utils::{required,implied}_predicates however, that should fix the regression.

[W95Psp]

Makes sense, thanks. Will add an option there.

[W95Psp]

I'm looking at adding an option, will probably push a PR soon

[Nadrieril]

Could you merge #1559 first to avoid the merge conflicts?

[W95Psp]

I had no time to look at it, looking at your PR now, but it seems unlikely we will merge it today.
On our end, releasing a new version is important for an issue we have in libcrux, thus sadly I think we'll need to merge that fix first. It is not very invasive though.

Also, your PR will require fixes on the engine (e.g. the Self: T bound change), so yeah, that's unlikely we can merge your PR first :/
Plus the fact I will need to regenerate hashes for libcrux.