Bug: `dyn` supertrait method dispatch reads the wrong vtable

[niooss-ledger]

Code snippet to reproduce the bug:

pub trait SuperA {
    fn meth_sup_1(&self) -> u32;
}
pub trait SubA: SuperA {
    fn meth_sub_2(&self, a: u64, b: u64) -> u64;
}

pub fn call_super_wrong_sig(obj: &dyn SubA) -> u32 {
    obj.meth_sup_1()
}

Charon version: 9dd7f23

Charon command: charon rustc --print-ullbc --ullbc -- --crate-type lib repro.rs

Charon output:

With --print-ullbc:

// Full name: repro::call_super_wrong_sig
pub fn call_super_wrong_sig<'_0>(obj_1: &'_0 (dyn SubA + '_0)) -> u32
{
    let _0: u32; // return
    let obj_1: &'3 (dyn SubA + '4); // arg #1
    let _2: &'5 (dyn SubA + '6); // anonymous local

    bb0: {
        storage_live(_2);
        _2 = &(*obj_1) with_metadata(copy obj_1.metadata);
        _0 = (copy ((*_2.metadata)).method_meth_sup_1)(move _2) -> bb2 (unwind: bb1);
    }

    bb1: {
        unwind_continue;
    }

    bb2: {
        storage_dead(_2);
        return;
    }
}

With --print-llbc:

// Full name: repro::call_super_wrong_sig
pub fn call_super_wrong_sig<'_0>(obj_1: &'_0 (dyn SubA + '_0)) -> u32
{
    let _0: u32; // return
    let obj_1: &'3 (dyn SubA + '4); // arg #1
    let _2: &'5 (dyn SubA + '6); // anonymous local

    storage_live(_2)
    _2 = &(*obj_1) with_metadata(copy obj_1.metadata)
    _0 = (copy ((*_2.metadata)).method_meth_sup_1)(move _2)
    storage_dead(_2)
    return
}

Explain the bug:

I believe Charon should generate ((*((*_2.metadata)).super_trait_1)).method_meth_sup_1 instead of ((*_2.metadata)).method_meth_sup_1.

For more details, I discussed with Claude Code (model claude-opus-4-8[1m]) and asked it to produce a short bug report. It created this Markdown file: BUG.md.

For information, I used some AI to find issues in Charon (which I am of course triaging/reviewing before sharing as GitHub issues). I actually was confused by the initial report of this issue, as the ULLBC code looked right at first glance (method method_meth_sup_1 is named correctly). And the fact that I am not so familiar with ULLBC notation combined with Aeneas not supporting function pointers did not help being sure there was an issue. Then I asked more details about the issue until I got a good understanding and created a short Rust reproducer.

[Nadrieril]

Oh, well spotted, the pass that adds these calls expects to only encounter uses of dyn Trait as Trait, but this is dyn Trait as Supertrait which throws it off.