Support for mutually recursive traits and functions

[msprotz]

I am getting this error:

   Compiling libcrux-ml-kem v0.0.2-pre.2 (/Users/jonathan/Code/libcrux/libcrux-ml-kem)
warning: Could not find clauses for trait obligations:core::ops::function::FnMut<Fold, (Acc, core::iter::adapters::enumerate::{impl core::iter::traits::iterator::Iterator for @Adt15<I>#1}<I>[@TraitClause0]::Item)>

         Available clauses:
         [@TraitClause0]: core::iter::traits::iterator::Iterator<I>
         [@TraitClause1]: core::ops::function::FnMut<Fold, (Acc, (usize, @TraitClause0::Item))>
         [@TraitClause2]: @TraitDecl21<R>
         [Self]: core::iter::traits::iterator::Iterator<@Adt15<I>>
         - context: core::iter::adapters::enumerate::{impl#1}::try_fold
 --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/iter/adapters/enumerate.rs:73:5

warning: Could not find clauses for trait obligations:core::ops::function::FnMut<Fold, (Acc, core::iter::adapters::enumerate::{impl core::iter::traits::iterator::Iterator for @Adt15<I>#1}<I>[@TraitClause0]::Item)>

         Available clauses:
         [@TraitClause0]: core::iter::traits::iterator::Iterator<I>
         [@TraitClause1]: core::ops::function::FnMut<Fold, (Acc, (usize, @TraitClause0::Item))>
         [Self]: core::iter::traits::iterator::Iterator<@Adt15<I>>
         - context: core::iter::adapters::enumerate::{impl#1}::fold
 --> /rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/iter/adapters/enumerate.rs:96:5

thread 'rustc' panicked at 'Invalid scc:
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}
libcrux_ml_kem::simd::portable::ntt_multiply
libcrux_ml_kem::simd::portable::deserialize_1
libcrux_ml_kem::simd::portable::deserialize_4
libcrux_ml_kem::simd::portable::deserialize_5
libcrux_ml_kem::simd::portable::deserialize_10
libcrux_ml_kem::simd::portable::deserialize_11
libcrux_ml_kem::simd::portable::deserialize_12
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::ntt_multiply
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_1
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_4
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_5
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_10
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_11
libcrux_ml_kem::simd::portable::{impl libcrux_ml_kem::simd::simd_trait::Operations for libcrux_ml_kem::simd::portable::PortableVector}::deserialize_12', src/reorder_decls.rs:642:13
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
warning: `libcrux-ml-kem` (lib) generated 2 warnings
error: could not compile `libcrux-ml-kem` (lib); 2 warnings emitted

steps to reproduce: clone libcrux with branch and commit information below, then run charon in the libcrux-ml-kem subdirectory

jonathan@benedictine:~/Code/libcrux/libcrux-ml-kem (franziskus/simd-ml-kem-architecture) $ git rev-parse HEAD
e3ab051c847df34f245fba39117c50ac6ffaebcf
jonathan@benedictine:~/Code/libcrux/libcrux-ml-kem (franziskus/simd-ml-kem-architecture) $ charon

for now, I would love to just get support in charon so that I can handle this in Eurydice and produce C code -- Aeneas support can come later

[R1kM]

After debugging a bit, I am not sure this is due to recursive functions or traits. Below is a minimized example leading to the same error. The problematic part is the Portable::ZERO() in the implementation of ntt_multiply, removing the Portable prefix makes the error go away.

trait Ops {
    fn ZERO() -> Self;
    fn ntt_multiply(&Self) -> Self;
}

struct Portable {}

fn ZERO() -> Portable {
    Portable {}
}

fn ntt_multiply(x: &Portable) -> Portable {
    let mut out = Portable::ZERO();
    out
}

impl Ops for Portable {
    fn ZERO() -> Self {
        ZERO()
    }

    fn ntt_multiply(x: &Self) -> Self {
        ntt_multiply(x)
    }
}

[Nadrieril]

After discussing with @R1kM I understand the issue better: this is a limitation put in place because verification backends typically don't support mutually recursive groups that mix e.g. trait impls and functions. At the very least we should have a clear error message.

At least for this case charon could do better: given how charon encodes trait impls, inside ntt_multiply, we don't actually need to refer to a trait impl to get the function Portable::ZERO; we could name it directly as test_crate::{impl test_crate::Ops for test_crate::Portable}::ZERO and avoid the issue.

[sonmarcho]

I think a first thing to do is to allow heterogeneous groups of mutually recursive definitions in Charon, and fail in Aeneas if such a group is not supported. I have several things in mind to add proper support in Aeneas: it depends on the cases we encounter. In particular, if we only encounter mutually recursive groups of functions and implementations I think it's ok.

[sonmarcho]

After discussion: we will add a pass to inline calls to methods when the implementation is known (i.e., it is not a trait clause). It should take care of most situations where we have a group of mutually recursive functions and implementations. If we encounter (real-world) cases which are not eliminated through this micro-pass, we will implement a more general solution.

[Nadrieril]

Btw this should no longer be a problem in Eurydice since #265 (and https://github.com/AeneasVerif/eurydice/pull/27). The proposed fix is still desirable for Aeneas but shouldn't be a blocker.