search

creusot-rs / creusot

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

Issue with invariants for mappings #866

Closed jhjourdan closed 1 month ago

jhjourdan commented 1 year ago

We don't enforce invariants for mappings, and the extentionnality law for them does not take invariants into account.

See https://github.com/xldenis/creusot/pull/865#issuecomment-1729463440 and the following comments.

Probably the most principled way to fix this would be to encode invariants in a way which is much closer to Why3's type invariants.

xldenis commented 1 year ago

Probably the most principled way to fix this would be to encode invariants in a way which is much closer to Why3's type invariants.

This would require eliminating clones as it means that the module defining the type needs to reference the invariant predicate itself. That just re-emphasizes how much we (I) need to eliminate cloning over the next few weeks.

jhjourdan commented 1 month ago

This is fixed by #1096. Mappings have valid as well as invalid values as keys.