Allow adt constructors to have associated axiom

[JonasAlaif]

The main advantage is that bounded types can be encoded as an adt. For example:

adt u8 {
  to_u8(from_u8: Int)
    axiom (0 <= from_u8 < 256)
}

which is encoded as (the 0 <= from_u8 < 256 ==> line and axiom { forall t: u8 :: { from_u8(t) } 0 <= from_u8(t) < 256 } axiom are new)

domain u8  {
  function to_u8(from_u8: Int): u8 
  function from_u8(t: u8): Int 
  function u8_tag(t: u8): Int 
  
  axiom {
    forall from_u8: Int :: { to_u8(from_u8) }
      // new implication
      0 <= from_u8 < 256 ==>
        from_u8 == from_u8(to_u8(from_u8))
  }
  // new axiom
  axiom {
    forall t: u8 :: { from_u8(t) }  0 <= from_u8(t) < 256
  }
  
  axiom {
    forall from_u8: Int :: { to_u8(from_u8) } u8_tag(to_u8(from_u8)) == 0
  }
  axiom {
    forall t: u8 :: { u8_tag(t) } { from_u8(t) } false || t == to_u8(from_u8(t))
  }
}

Previously, one could try defining the regular adt and separately a 0 <= from_u8(t) < 256 axiom. However, this would be unsound as without the ==> we would get e.g. -1 == from_u8(to_u8(-1)) and 0 <= from_u8(to_u8(-1)) < 256. This PR solves this, since the ==> eliminates the injectivity fact in that case.

This feature is still dangerous in one specific case: it is unsound to write an unsatisfiable axiom (i.e. axiom (false) or equivalent). This would result in an axiom { forall t: _ :: false } in the encoded domain. The use of the axiom keyword should make this clear to users.

[alexanderjsummers]

This is a cool feature! Will/could there be a check that when applying the constructor, this property holds? e.g. if I apply to_u8(-1) can I avoid accidentally assuming false?

I would be in favour of having such a feature; I'd also consider calling it by a different keyword (especially if we add a check on construction); maybe an invariant or a refinement?

[JonasAlaif]

@alexanderjsummers you do not accidentally assume false when writing to_u8(-1), this PR specifically tries to avoid that by instead giving you an uninterpreted u8. That is, the following holds 0 <= from_u8(to_u8(-1)) < 256 but you do not know which u8 you got (and specifically you do not get from_u8(to_u8(-1)) == -1 which would let you prove false).

I like the axiom keyword since it very closely matches the domain axiom that is generated, in the above example axiom (0 <= from_u8 < 256) results in:

axiom {
  forall t: u8 :: { from_u8(t) }  0 <= from_u8(t) < 256
}

Regarding a checked "invariant": I'm not against doing that, but it doesn't match the current adt design where field accesses are also not checked. When accessing x.value field of an adt Option[T] { Some(value: T) None() } we are not required to prove that x.isSome (and get an uninterpreted T in the case that x.isNone). Imo if we wanted that then we should have e.g. a checked adt ... or something which adds the checks for constructors (that the user-written invariant holds) and checks on field accessors (that the correct tag is set).

[ArquintL]

@JonasAlaif Looking a the first axiom in the encoding, it seems to me that this PR basically restricts the injectivity axiom that would normally be generated for each adt constructor. I'm wondering about the expressiveness of the proposed language feature. It seems to nicely cover the mentioned use case of bounded types but thinking of, e.g., an adt constructor with 2 parameters that is injective up-to-commutativity, I don't think this solution would be expressive enough or am I wrong? (The use case in one of my projects was an ADT of labels, where you have a leaf label constructor as well as join and intersection constructors each taking two labels as parameters for which the order of parameters does not matter). In this context, there's an on-going BSc thesis by @Ennster supervised by @mschwerhoff that explores an alternative solution to my problem, namely using equality on the ADT purely syntactically and express all other properties via a dedicated equivalent function

[mschwerhoff]

The thesis already mentioned by @ArquintL is due by end of May, and I suggest to put this PR on hold until the results from the thesis have been written up (assuming the PR is not time-critical). Other than that, I am all in favour of an extension that enables complementing ADTs with additional theories.

[mueller55]

Sorry that it took me so long to look into this proposal. I am wondering what the most natural design is to achieve our goals. For the motivating examples that @JonasAlaif mentioned, it seems we could allow refinement types in ADTs. Then the axiomatization should follow naturally. In particular, refinement types become preconditions for constructors and postconditions for selectors, which we should encode analogously to contracts for heap-dependent functions.

A key difference to @JonasAlaif's design is that the constraints are then per constructor parameter rather than per ADT. I think that matches well, because ADT values do not have state.

An open question with my idea is whether one would allow only simple refinement types or also dependent types, which could relate multiple arguments of the same constructor. The former seems enough for @JonasAlaif's use cases.

By the way, I thjnk adding refinement types to Viper in general might be worthwhile; Anqi plans to look into this.