Collections cannot have Negative Length

[DavePearce]

Currently, the following example fails because the theorem prover considers a negative length for the collection is possible:

nat f([int] xs):
    return |xs|

[DavePearce]

Problem with this is: where do I generate that constraints?

If I want to generate it when I encounter LengthOf expressions in WYCS, then I need a way to traverse an arbitrary expression and dig it out. That is possible with some kind of xpath-style expression ... but that sounds expensive.

Really, what would make a lot of sense would be to simply generate that constraint in VerificationCheck, where we know which variables may have collection type.

[DavePearce]

Have been working on this using the following rule:

 infer ZeroLessThan(Sum[real x1, {|Mul[real x2, {|LengthOf l, AExpr... bs|}], AExpr... cs|}] s):
     => let ieq1 = ZeroLessThan(s), // annoying
            ieq2 = ZeroLessThan(Sum[1.0,{|Mul[1.0,{|l|}]|}])
        in And { ieq1, ieq2 }, if (x2 != 1.0 || x1 <= 0.0 || |bs| > 0 || |cs| > 0)

Currently, it loops infinitely though. I think the reason is that it matches itself.