NonZero types are used in programs that want to also leverage the type system to prove correctness and to get layout optimizations. Currently View and DeepModel are not implemented for the type.
This appeared easy enough to add myself but I've hit a weird error:
no method named `__creusot_view_stub` found for type parameter `T` in the current scope
It's unclear why this happens since ZeroablePrimitive is refined to require View and DeepModel so these bounds should be implied but it still behaves as if they weren't. That method is implemented for all types implementing View, so should be available.
The code I tried: https://github.com/Kixunil/creusot/pull/1/changes#diff-395074bc7336c8f926175cd143cf9f44ca74b57af5bf866708883b2f578be005 (Don't bother reading PR comments and other files. I used clanker to help me write the code but I did steer it heavily and reviewed the code myself. I'm stuck here too as a human.)
Figured it out.
NonZerotypes are used in programs that want to also leverage the type system to prove correctness and to get layout optimizations. CurrentlyViewandDeepModelare not implemented for the type.This appeared easy enough to add myself but I've hit a weird error:It's unclear why this happens sinceZeroablePrimitiveis refined to requireViewandDeepModelso these bounds should be implied but it still behaves as if they weren't. That method is implemented for all types implementingView, so should be available.The code I tried: https://github.com/Kixunil/creusot/pull/1/changes#diff-395074bc7336c8f926175cd143cf9f44ca74b57af5bf866708883b2f578be005 (Don't bother reading PR comments and other files. I used clanker to help me write the code but I did steer it heavily and reviewed the code myself. I'm stuck here too as a human.)Figured it out.