Skip to content

Bug: returning impl Iterator + '_ whose closure derefs a captured reference: "Internal error" #1207

Description

@oliver-butterley

E.g.,

pub struct T { scale: u8, data: [u8; 8] }
impl T {
    pub fn scaled(&self) -> impl Iterator<Item = u8> + '_ {
        self.data.iter().map(move |&b| b * self.scale)
    }
}

or more concisely yet still producing the same error:

pub fn f(x: &u8) -> impl Iterator<Item = u8> + '_ {
    (0..1).map(move |_| *x)
}

Both cause Aeneas to produce the error [Error] Internal error, please file an issue (Compiler source: interp/InterpProjectors.ml, line 544).

Aeneas version: b059c34
Charon version: 0.1.223

Seen in curve25519-dalek Scalar::bits_le scalar.rs:873-881

/// Get the bits of the scalar, in little-endian order
pub(crate) fn bits_le(&self) -> impl DoubleEndedIterator<Item = bool> + '_ {
    (0..256).map(|i| {
        ((self.bytes[i >> 3] >> (i & 7)) & 1u8) == 1
    })
}

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions