Proper way of having an abstract function as a postcondition of another abstract function?

[jad-hamza]

I'm trying to define a trait which contains a function inv and a function f that shows that inv is true.

trait PostOfAbstract {
  def inv(): Boolean = (??? : Boolean)

  def f(): Unit = {
    (??? : Unit)
  } ensuring(_ => inv())
}

I'm getting this invalid VC, any idea how to fix it? I was thinking the postcondition of f$27 should hold since it calls f$29, which has the same postcondition.

[ Debug  ] Symbols before PartialEvaluation
[ Debug  ] 
[ Debug  ] -------------Functions-------------
[ Debug  ] @derived(f$29)
[ Debug  ] def f$27(thiss$6: PostOfAbstract$0): Unit = {
[ Debug  ]   f$29(@unchecked {
[ Debug  ]     assert(thiss$6 is PostOfAbstractExt$0, "Cast error")
[ Debug  ]     thiss$6
[ Debug  ]   })
[ Debug  ] } ensuring {
[ Debug  ]   (x$1$9: Unit) => inv$5(thiss$6)
[ Debug  ] }
[ Debug  ] 
[ Debug  ] @extern
[ Debug  ] @derived(f$27)
[ Debug  ] @synthetic
[ Debug  ] def f$29(thiss$10: PostOfAbstract$0): Unit = {
[ Debug  ]   require(thiss$10 is PostOfAbstractExt$0)
[ Debug  ]   <empty tree>[Unit]
[ Debug  ] } ensuring {
[ Debug  ]   (x$1$9: Unit) => inv$5(thiss$10)
[ Debug  ] }
[ Debug  ] 
[ Debug  ] @derived(f$27)
[ Debug  ] def f$28(thiss$8: PostOfAbstract$0): Unit = {
[ Debug  ]   <empty tree>[Unit]
[ Debug  ] } ensuring {
[ Debug  ]   (x$1$9: Unit) => inv$5(thiss$8)
[ Debug  ] }
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Not printing symbols after PartialEvaluation as they did not change
[ Debug  ] 
[ Debug  ] 
[ Debug  ] Ensuring well-formedness after phase PartialEvaluation
[  Info  ]  - Checking cache: 'precond. (call f$29(@unchecked { ...)' VC for f @4:3...
[  Info  ] Cache hit: 'precond. (call f$29(@unchecked { ...)' VC for f$27 @4:3...
[  Info  ]  - Checking cache: 'postcondition' VC for f @4:3...
[  Info  ] Cache miss: 'postcondition' VC for f$27 @4:3...
[  Info  ]  - Now solving 'postcondition' VC for f$27 @4:3...
[  Info  ]  - Result for 'postcondition' VC for f$27 @4:3:
[Warning ]  => INVALID
[Warning ] Found counter-example:
[Warning ]   thiss$6: PostOfAbstract$0 -> PostOfAbstractExt$0(0)

[samarion]

Maybe the simplifier is messing up somewhere. Can you print the VC?

[jad-hamza]

Yes you're right, it seems the call to f$29 is simplified away, the VC is just:

[ Debug ] inv$5(thiss$6)

[jad-hamza]

The ensuring of f$29 disappears at some point (not sure where yet), so the simplifier thinks that f$29 is pure and drops the call.

[samarion]

This is due to the encoding replacing ensuring in abstract functions by chooses which are then dropped by the simplifier. We already had another issue reported because of this I think.

I'm thinking of a fairly major redesign of the simplifier to correctly take dependent types into account, but this will take some time. For a quick fix, we can maybe change the InoxEncoder (or wherever the NoTree is removed) to introduce an ensuring in addition to the choose in abstract functions.

[jad-hamza]

This one #408?
Thanks I'll try the fix

[romac]

This seems to be fixed on latest master, likely by #408.

[info] [  Info  ]   ┌───────────────────┐
[info] [  Info  ] ╔═╡ stainless summary ╞════════════════════════════════════════════════════════════════════════════╗
[info] [  Info  ] ║ └───────────────────┘                                                                            ║
[info] [  Info  ] ║ $init$0  precond. (call $init$2(@unchecked { ...)  valid  nativez3  ../../test.scala:1:22  0.142 ║
[info] [  Info  ] ║ f$30     postcondition                             valid  nativez3  ../../test.scala:4:3   0.116 ║
[info] [  Info  ] ║ f$30     precond. (call f$32(@unchecked { ...)     valid  nativez3  ../../test.scala:4:3   0.013 ║
[info] [  Info  ] ║ inv$6    precond. (call inv$11(@unchecked { ...)   valid  nativez3  ../../test.scala:2:3   0.015 ║
[info] [  Info  ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[info] [  Info  ] ║ total: 4    valid: 4    (0 from cache) invalid: 0    unknown: 0    time:   0.286                 ║
[info] [  Info  ] ╚══════════════════════════════════════════════════════════════════════════════════════════════════╝

[jad-hamza]

Or maybe epfl-lara/inox#96, thanks for keeping track!