Problems with FlightManager.flint

[wmanshu]

contract FlightManager {
  var flightInformation: FlightInformation
  let admin: Address
  var ticketPrice: Int

  var numRemainingSeats: Int
  var totalSeats: Int
  var passengers: [Address] = []
  var numPassengers: Int = 0
  var amountPaid: [Address: Wei] = [:]

  invariant (forall (a, Address, dictContains(amountPaid, a) ==> amountPaid[a].rawValue == ticketPrice))
  invariant (forall (a, Address, 0 < a  ==> a > 0)
  invariant (...)
}

• the first invariant (forall (a, Address, dictContains(amountPaid, a) ==> amountPaid[a].rawValue == ticketPrice)) uncommented with the verifier:
  ERROR:

couldn't get scope context of current function - used for updating shadow variable
Fatal error: file /home/manshu/flint/Sources/Verifier/Boogie/Statement+Expression.swift, line 991

• comment out the first invariant and not skipping the verifier: Contract specification verified!

• Problem with second invariant: Expected 'invariant' declaration within contract

• get similar problem as the first invariant in StandardToken.flint when writing the invariant forall (a, Address, balances[a] >= 0)

[wmanshu]

Also, a precondition is also causing problem

  @payable
  public func buy(implicit value: Wei)
   mutates (amountPaid, numPassengers, numRemainingSeats, passengers, Wei.rawValue)
    pre (dictContains (amountPaid, caller))  
    ...
  {
    let amountGiven: Int = value.rawValue
    // Record the received Ether in the contract's state.
    amountPaid[caller].transfer(source: &value)
    passengers[numPassengers] = caller
    numPassengers += 1
    numRemainingSeats -= 1
  }

If we have this pre-condition dictContains (amountPaid, caller) here, even if we skip the verifier, still causes a fatal error:
Fatal error: file /home/manshu/flint/Sources/IRGen/Preprocessor/IRPreprocessor+Expressions.swift, line 196

We cannot just remove this line, as it is required to pass the verification test

[mrRachar]

For currently unknown reasons, you can fix the dictContains (...) issue by equating it, i.e. dictContains (...) == true

[mrRachar]

Unfortunately also, transfer doesn't prove anything, and there are a number of issues that prevent it from doing so:

1. All implementations of Wei.transfer are defined on trait Asset. As this is a trait, it shouldn't in theory have access to the Wei's private variables, so all we can do in trait-level methods is state facts about its public interface. This won't work though as the getRawValue method is a method, and as with Implementation required for using return value in pre/post conditions  #446 this it is not currently possible to call this within the verification system.
   There is however a solution, you can actually assert things about the private fields of Wei in Asset's methods' post-conditions, due to the lack of any privacy checking within the verifier. This, however, would break quickly if anyone else implemented Asset and didn't use the internal name rawValue exactly the same or at all, and so this is extremely hacky.

2. Implementing the functions at the Wei level breaks many, many things, as most of the entire pipeline has this expectation that Wei is an Asset, and if you overload an implemented Asset's functions you get further issues, such as double definitions of the method across the codebase and in the generated output, which prevents Boogie from running the programme as just the first problem (this could in theory be the fix, by implementing a new language feature (or fixing a broken old one if this at one point did work) to allow overloading implemented trait methods)

3. Even if we can implement post-conditions, it turns out what these post-conditions should be is quite difficult to define. The most obvious one is

   func transfer(source: inout Self, amount: Int)
     post (source.rawValue == prev(source.rawValue) - amount)
     post (self.rawValue == prev(self.rawValue) + amount)
   
   func transfer(source: inout Self)
     post (source.rawValue == 0)

   but this has an obvious problem, what if source and self are the same? Then you'll end up with the post-conditions failing. So, let's try again, what if we did

   func transfer(source: inout Self, amount: Int)
     post (self.rawValue + source.rawValue 
             == prev(self.rawValue) +  prev(source.rawValue))

   but now we can't say anything about how those values have changed, and how amount affects it. This makes it impossible to create a useful post-condition for the second one (apart from the above again), and more importantly, it doesn't provide us any more information where used to write post-conditions for the side-effects of other functions.
   So, what's the alternative? We somehow try and make sure self and source are separate? One option might be to fatalError if they're the same. The problem with this is that two Wei are incomparable (and this might be difficult to implement). Alternatively, we could add an extra proof obligation onto the call-site, requiring them to prove that they are different. The concern here is that it might be really quite difficult to prove, seeing as the call-site too wouldn't be able to check for Wei inequality.
   The best I can come up with is

   func transfer(source: inout Self, amount: Int)
     post (source.rawValue == prev(source.rawValue) - amount
             && self.rawValue == prev(self.rawValue) + amount
             || self == source)
   
   func transfer(source: inout Self)
     post (source.rawValue == 0 || source == self)

   which will work well, and force people to consider the source==self case, but this still forces the programmer to try and work out if the two Wei are separate, or let things propagate, and even this simpler solution has required modifications to be made to the verification system to allow self to exist as a instance map index (and thus technically allows self == <int>)