I have not yet found what exactly causes it, but here's a reasonably small reproduction example:
src/lib.rs
src/x.rs
use creusot_std::prelude::{Int, logic, View};
pub struct Foo(u128);
impl Foo {
pub const ZERO: Self = Foo(0);
}
impl View for Foo {
type ViewTy = Int;
#[logic]
fn view(self) -> Self::ViewTy {
self.0.view()
}
}src/y.rs
use creusot_std::prelude::{ensures, Int, logic, View};
use crate::x::Foo;
pub struct Bar(Foo);
impl Bar {
pub const ZERO: Self = Bar(Foo::ZERO);
}
impl View for Bar {
type ViewTy = Int;
#[logic]
fn view(self) -> Self::ViewTy {
self.0.view()
}
}
#[logic]
#[ensures(Bar::ZERO@ == 0)]
fn check_zero() {}This emits ERROR_UNBOUND into the Coma:
constant const_ZERO: t_Bar = [%#sy'2] { f0 = { ERROR_UNBOUND_f0 = (0: UInt128.t) } }
Also happens when trying to initialize the consts using const functions.
I'm using commit de3ae4b which I hope is recent enough for a bug report. I looked into the history and didn't see anything relevant.
Side question: would it make sense to allow #[ensures] on constants? It seems that #[ensures(ZERO@ == 0)] would make sense so that wherever the constant is used the assumption is imported.
I have not yet found what exactly causes it, but here's a reasonably small reproduction example:
src/lib.rssrc/x.rssrc/y.rsThis emits
ERROR_UNBOUNDinto the Coma:Also happens when trying to initialize the consts using
constfunctions.I'm using commit de3ae4b which I hope is recent enough for a bug report. I looked into the history and didn't see anything relevant.
Side question: would it make sense to allow
#[ensures]on constants? It seems that#[ensures(ZERO@ == 0)]would make sense so that wherever the constant is used the assumption is imported.