Disallow nonpositive fractions

[necto]

Does VeriFast support predicates with permission 0.0 (e.g. [0.0]character(p, _))?

If it does, how can one summon such an instance at a given address? Or how can one slice off a 0.0 portion of an existing instance?

If it does not, how can one prove that in [?frac]character(p, _) 0.0 < frac ?

Also is there a way to prove that a fraction is non-negative?

[btj]

Semantically, [f]character(p, _) implies 0 < f <= 1. In other words, [0]character(p, _), [-1]character(p, _), and [1.1]character(p, _) are all equivalent to false. This is true for all pointee predicates (anything that can be written as E |-> _ for some lvalue E). (This does not hold for user-defined predicates: it's fine to write predicate foo() = true; and close [0]foo();.)

VeriFast already produced 0 < f when producing [f]E->F |-> pat. I just pushed a commit (51f686a) such that it does so when producing [f]E |-> pat as well, where E is either a global variable or of the form *E'.

I guess that resolves your issue; if not, feel free to reopen.

[necto]

Why does it not hold for "non pointee" predicates?
I am trying to prove a factoid like this lemma:

  lemma void foo(void* x, predicate (void*;t) p)
  requires [?f]p(x, _);
  ensures (f == 0 ? true : [f]p(x,_));
  {
  }

Verifast complains here, that foo leaks chunks, in the case where f == 0. Why doesn't it discard this branch as unfeasible?

[btj]

As I wrote before, VeriFast doesn't keep you from defining a predicate predicate quux() = true; and then doing close [0]quux();. Your lemma does not hold for all predicates.

Why did I make the decision to allow this? Not because I think that scenario is particularly useful; I simply saw no compelling reason to forbid it at the time.

[necto]

Alright, so my takeaway:

Semantically, [f]character(p, _) implies 0 < f <= 1.

but [f]quux(p, _) does not constrain f in any way, if quux is not any of the basic built-in predicates.

How difficult is it to make [f]quux(p, _) imply 0 < f <= 1 universally?
Do you think that might brake existing proofs?

Btw, I have no button to reopen the issue here, but that's fine.

[btj]

That's right.

Making it imply f <= 1 universally would be non-trivial, I think. Consider predicate foo(char *p; char c) = [1/2]*c |-> v;. You can legitimately have two [1]foo(p, c) chunks around at the same time. Currently, they would be merged into a [2]foo(p, c) chunk. To prevent that from happening, you would have to impose a f1 + f2 <= 1 proof obligation before merging two fractional chunks, which I think would be bothersome in some scenarios.

Making it imply 0 < f universally seems unproblematic. I'm not aware of any use cases for nonpositive fractions. Making this change would involve imposing a proof obligation of 0 < f on close [f]p(...); and producing a 0 < f assumption when producing [f]p(...). This would impose a slight extra burden on the SMT solver but it's probably negligible.

Would just 0 < f solve your problem? Also, could you give just a bit of detail on the scenario that it enables?

[necto]

I am trying to optimize the contracts for my implementation of a fixed size vector: https://gist.github.com/necto/bd58fd59f80b679f922f021566b1dcbb

Currently, it has somewhat "ugly" lines, like
https://gist.github.com/necto/bd58fd59f80b679f922f021566b1dcbb#file-vector-c-L280
and
https://gist.github.com/necto/bd58fd59f80b679f922f021566b1dcbb#file-vector-c-L301

I think those lines won't be needed once all the fractions are assumed to be positive.
But that is not a big deal, just a bit of perfectionism :)

P.S. if you want to run the files from the gist in verifast, here are the headers they include: https://github.com/vignat/vignat/tree/master/nf/lib/containers