stainless
stainless copied to clipboard
epfl-lara
Incorrect ADT member type approximation
Seems like Stainless approximate the type of FunDef.tp to Type at some point, and then can't prove it's actually a FunType.
object Test:
sealed trait Type
final case class AtomType(i: BigInt) extends Type
final case class FunType(args: List[Type], res: Type) extends Type
final case class FunDef(tp: FunType)
def arity(funs: List[FunDef], i: BigInt) =
require(i >= 0 && i < funs.length)
val funDef: FunDef = funs(i)
funDef.tp.args.length
[Warning ] - Result for 'cast correctness' VC for arity @16:5:
[Warning ] i < BigInt("0") || i >= length[FunDef](funs) || apply[FunDef](funs, i).tp.isInstanceOf[FunType]
[Warning ] enumSubtype.scala:16:5: => TIMEOUT
funDef.tp.args.length
^^^^^^^^^^^^^^
[ Info ] Verified: 1 / 2
[ Info ] Done in 12.58s
[ Info ] ┌───────────────────┐
[ Info ] ╔═╡ stainless summary ╞═════════════════════════════════════════════════════════════════════════════════╗
[ Info ] ║ └───────────────────┘ ║
[ Info ] ║ enumSubtype.scala:15:26: arity precond. (call apply[FunDef](funs, i)) valid U:smt-z3 0.1 ║
[ Info ] ║ enumSubtype.scala:16:5: arity cast correctness timeout U:smt-z3 2.0 ║
[ Info ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[ Info ] ║ total: 2 valid: 1 (0 from cache, 0 trivial) invalid: 0 unknown: 1 time: 2.10 ║
[ Info ] ╚═══════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Verification pipeline summary:
[ Info ] anti-aliasing, smt-z3, non-batched
[ Info ] Shutting down executor service.
Removing extends Type after FunType solves the problem.
Works if my FunDef's not in a List or, is accessed through a fixed index:
object Test2:
sealed trait Type
final case class AtomType(i: BigInt) extends Type
final case class FunType(args: List[Type], res: Type) extends Type
final case class FunDef(tp: FunType)
def arity(funs: List[FunDef]) =
require(funs.length > 0)
val funDef: FunDef = funs(0)
funDef.tp.args.length
[ Info ] Verified: 2 / 2
[ Info ] Done in 11.63s
[ Info ] ┌───────────────────┐
[ Info ] ╔═╡ stainless summary ╞════════════════════════════════════════════════════════════════════════════════════╗
[ Info ] ║ └───────────────────┘ ║
[ Info ] ║ enumSubtype.scala:15:26: arity precond. (call apply[FunDef](funs, BigInt("0"))) valid U:smt-z3 0.0 ║
[ Info ] ║ enumSubtype.scala:16:5: arity cast correctness valid U:smt-z3 0.1 ║
[ Info ] ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
[ Info ] ║ total: 2 valid: 2 (0 from cache, 0 trivial) invalid: 0 unknown: 0 time: 0.12 ║
[ Info ] ╚══════════════════════════════════════════════════════════════════════════════════════════════════════════╝
The problem is ADT constructor types don't exist in SMT world so we have to encode FunType into {x: Type | x is FunType }.
The way Inox handles refinement types in ADTs is by progressively unfolding the type and asserting at each step that it is constructed from well-typed sub-components. That's why it works for the constant index 0: Inox unfolds funs just once and you get all the right assertions to prove that funDef.tp has the right type. I expect that if you replaced 0 with 100 it would also timeout because Inox would need to perform 100 unfoldings before it had enough information to prove the property.
This could be fixed by injecting type assumptions in more places, but this would need to be done deep inside the template unfolding implementation...
A possible workaround is to define your own def getFunType(fd: FunDef): FunType = fd.tp method because IIRC dependent types are assumed on function invocation results.
