search

viperproject / prusti-dev

A static verifier for Rust, based on the Viper verification infrastructure.
http://prusti.org
Other
1.52k stars 102 forks source link

Updated snapshot injectivity axiom. #1475

Closed zgrannan closed 7 months ago

zgrannan commented 7 months ago

The snapshot domain axioms do not currently ensure that a snapshot for a variant must correspond to a constructor invocation. As a consequence, given snapshots s1 and s2 that return the same values for all field access functions, we cannot prove s1 == s2 (see the included test).

This PR introduces a new injectivity axiom, asserting that each variant snapshot corresponds to a constructor invocation:

forall this: Variant :: 
  {field1(this), field2(this), ...}
  this == cons(field1(this), field2(this), ...)

The replaces the current injectivity axiom:

forall _l_args..., _r_args... :: {cons(_l_args...), cons(_r_args)}
    cons(_l_args...) == cons(_r_args) ==> _l_args... == _r_args...

The trigger on field access axioms is also made more permissive. This is necessary because the new injectivity axiom is only triggered on field access (and not on snapshot construction).

Previous: forall args... :: {field(cons(arg_field, other_args...))} field(cons(arg_field, other_args...)) == arg_field New: forall args... :: {cons(arg_field, other_args...)} field(cons(arg_field, other_args...)) == arg_field

Finally, DefinitionCollector is updated to ensure that functions used in the triggers of domain axioms are always preserved.