Open msprotz opened 2 months ago
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)
}
}
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.
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.
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.
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.
I am getting this error:
steps to reproduce: clone libcrux with branch and commit information below, then run
charon
in the libcrux-ml-kem subdirectoryfor 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