creusot-rs / creusot

Creusot helps you prove your code is correct in an automated fashion.
GNU Lesser General Public License v2.1
1.12k stars 50 forks source link

MLCFG error on derefing `Arc`/`Rc` in contracts #814

Open sarsko opened 1 year ago

sarsko commented 1 year ago
#[requires((*a)@ == 0)]
fn test_arc(a: Arc<usize>) {}

gives: File "../pt.mlcfg", line 53, characters 77-89: unbound function or predicate symbol 'Deref0.deref'

Same error for Rc.

xldenis commented 1 year ago

I think this is from using * in the contract which is unsupported. It should error at the pearlite level though

sarsko commented 1 year ago

Both of these are allowed through:

#[requires((*v)@ == 0)]
fn test_box(v: Box<usize>) {}

#[requires(*v == 0usize)]
fn test_usize(v: &usize) {}
xldenis commented 1 year ago

& and Box have special built-in behavior. I agree we should add an instance of Shallow and Deep model for Arc and Rc though.