Implementation required for using return value in pre/post conditions

[wmanshu]

 func factorial(n: Int) -> Int
  post (n < 2 ==> (returns (1)))
  post (n >= 2 ==> (returning (r, r == n * factorial(n - 1))))
  {
    if (n < 2) { return 1 }
    return n * factorial(n: n - 1)
  }

In file factorial.flint, it is difficult to write a post condition in the case n>= 2. returning (r, r == n * factorial(n - 1)), this throws an error

Also similar examples in Voting.flint

public func getWinningProposalName() -> String
  {
    return proposals[getWinningProposalID()].name
  }

[wmanshu]

one more example from flintDAO.flint

  public func executeProposal()
{
  ...
    if proposals[proposal].yea > proposals[proposal].nay {
       ...
       let totalstake: Int = getTotalStake()
       for let value: Wei in balances {
         let rawvalue: Int = (proposals[proposal].payout * value.rawValue) / totalstake
          ...
       }  
       ...
    }
}

To avoid potential divide-by-zero error, we want a condition to say that getTotalStack() > 0. But when putting it as a precondtion, it gives Flint to Boogie translation error

[mrRachar]

After some discussion, we've come to the conclusion that this should not be implemented in the verification subset of the language, as it would rely on the other functions working, and so could easily produce false positives/negatives. Also, it seems against the idea of verification, surely you're not wanting to check that factorial is n * factorial(n - 1) because that is literally just the same as the code, instead you'd want to check that factorial is the product of all the numbers up to and including n.

Therefore, to allow more mathematical verification there are plans to implement product(...) and sum(...) functions, or a single reduce(op, ...) function, which can take in literal ranges or identifiers of arrays and allow you to verify these functions properly.

As for the other example, you might have to store that as a field for now to be able to verify it. Obviously, if @SusanEisenbach thinks it would be better done by creating a system for Flint function calls in Boogie, then this will be implemented.

[SusanEisenbach]

For now don’t do anything. We should have a brainstorming session when both Sophia and I are back. Susan

…

-- Professor Susan Eisenbach Department of Computing Imperial College London On 5 Aug 2019, at 16:46, mrRachar <[email protected]<mailto:[email protected]>> wrote: After some discussion, we've come to the conclusion that this should not be implemented in the verification subset of the language, as it would rely on the other functions working, and so could easily produce false positives/negatives. Also, it seems against the idea of verification, surely you're not wanting to check that factorial is n * factorial(n - 1) because that is literally just the same as the code, instead you'd want to check that factorial is the product of all the numbers up to and including n. Therefore, to allow more mathematical verification there are plans to implement product(...) and sum(...) functions, or a single reduce(op, ...) function, which can take in literal ranges or identifiers of arrays and allow you to verify these functions properly. As for the other example, you might have to store that as a field for now to be able to verify it. Obviously, if @SusanEisenbach<https://github.com/SusanEisenbach> thinks it would be better done by creating a system for Flint function calls in Boogie, then this will be implemented. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub<#446?email_source=notifications&email_token=ABC6SZWPQERGS5MZ5E7LJD3QDBDOZA5CNFSM4IISIC5KYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOD3SHOTI#issuecomment-518289229>, or mute the thread<https://github.com/notifications/unsubscribe-auth/ABC6SZQF4UB6RXKL66RRZDTQDBDOZANCNFSM4IISIC5A>.