Potential Boogie limitation for simple assertions on contract and struct properties

[matteobilardi]

In both of these snippets, one would expect the assertion to be verified as the contract/struct property is set to zero upon initialisation and there are no declared methods that later modify such property.

contract Assert {
  var i: Int
}

Assert :: (any) {
  public init() {
    i = 0
  }

  public func failIfNotZero() {
    assert(self.i == 0)
  }
}

The Boogie translation for the previous code looks valid, however, the assertion cannot be verified by boogie. This is also the case for a similar struct:

struct Assert {
  var x: Int = 0

  public func failIfNotZero() {
    assert(self.x == 0)
  }
}

I initially speculated that the translation might be failing to keep track of initialisation, but that is certainly not the case for structs as the boogie translation explicitly requires that the struct instance on which a struct method is being called be among the ones which have been initialised so far. Thus, I fear that this might be either some boogie limitation or some unidentified conceptual issue with the current translation. In both cases, this issue needs further research.

[matteobilardi]

Inability to keep track of initialisation in the Boogie translation

In a similar manner, the assertion in the following contract also fails.

contract Assert {
  var initialized: Bool = true
}

Assert :: (any) {
  public init() {}

  public func isInitialized() {
    assert(initialized)
  }
}

Currently, the Flint contract above gets translated for verification into the Boogie code below (once the Flint stdlib and all the checks on assets have been removed for clarity).

var initialized_Assert: bool;

procedure {:inline 10} init_Assert()
  modifies initialized_Assert;
{
    initialized_Assert := true;
}

procedure {:inline 10} isInitialized_Assert()
{
  assert (initialized_Assert);
}

However, such a translation fails to keep track of the fact that when the isInitialized method gets called on the singleton instance of the Assert contract, the init method must have already been called exactly once at some point in the past. The lack of this information causes the initialized contract property to assume any arbitrary value when isInitialized is called, thus, the assertion cannot be verified.

Even though I believe there should be a way to encode this information through the verifier language, with my current understanding of Boogie, I cannot think of a valid one: e.g. assigning an initial value to the initialized property in the global scope and immediately after declaration (initialized_Assert := false;) does not constitute valid Boogie code.