Set and Sequence axiomatisation incompletenesses

Use the m03/m04 and adapted variants in the issue as minimal reproductions, comparing the cases marked Fails and Passes. Trace the Set and Seq axiomatisation used by Silver's verifier; done means the incompleteness is characterized and the affected verification behavior is corrected with regression coverage.

Created by @mschwerhoff on 2015-06-10 07:25
Last updated on 2019-05-16 13:37

#!text

method m03(S1: Seq[Ref], S2: Set[Ref], x: Ref)
  requires S1 == Seq(x) && S2 == Set(x)
  requires forall i: Int :: i in [0..|S1|) ==> S1[i] != null
  ensures  forall y: Ref :: y in S2 ==> y != null /* Fails */
{}

method m04(S1: Seq[Ref], S2: Set[Ref], x: Ref)
  requires S1 == Seq(x) && S2 == Set(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  forall y: Ref :: y in S2 ==> y != null /* Fails */
{}

method m03simplified(S1: Seq[Ref], x: Ref)
  requires S1 == Seq(x)
  requires forall i: Int :: i in [0..|S1|) ==> S1[i] != null
  ensures  x != null /* Fails */
{}

method m04simplified(S1: Seq[Ref], x: Ref)
  requires S1 == Seq(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails */
{}

method m04adapted(S1: Set[Ref], x: Ref)
  requires S1 == Set(x)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails */
{}

method m04adaptedWithProperty(S1: Set[Ref], x: Ref)
  requires S1 == Set(x)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Passes */
{}

method m04adaptedWorse(S1: Set[Ref], x: Ref, a: Ref)
  requires S1 == Set(x,a)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Fails in Silicon, but not in Carbon (?) - probably expected to fail */
{}

method m04adaptedWorseWithFurtherProperty(S1: Set[Ref], x: Ref)
  requires S1 == Set(x,x)
  requires forall z: Ref :: {Set(z)} z in Set(z)
  requires forall s1: Set[Ref], s2: Set[Ref], w:Ref :: {w in s1, (s1 union s2)} w in (s1 union s2) <==> (w in s1) || (w in s2)
  requires forall y: Ref :: y in S1 ==> y != null
  ensures  x != null /* Passes */
{}