When calling a node with a contract, guarantee is not always provable

Question

When calling a node with a contract, guarantee is not always provable

amosr opened this issue 3 years ago · 14 comments

Hi Daniel,

I'm running into some trouble using contracts. Sometimes when I have a node with a guarantee like:

node contracted(inp: EMA_INPUT) returns (ok: bool)
(*@contract
  guarantee P(inp, ok);
*)

for some predicate P, then, when I call this node from another node, I expect P(the_input, contracted(the_input)) to be trivially provable:

node caller(...) returns (...)
let
  x = contracted(f(i));
  --%PROPERTY P(f(i), contracted(f(i));
tel

but it seems like when the caller gets complicated, Kind2 can't always prove P.

I actually expected the caller of the contract to behave as if the guarantees of the contracts it calls were asserted (something like always(assume) => always(guarantee)), that is, I expected the contract caller above to desugar to something like:

node caller(...) returns (...)
let
  x = contracted(f(i));
  assert P(f(i), contracted(f(i));
tel

I've found some cases, however, where I can't prove some facts that rely on P, but asserting P in the caller lets me prove what I want.

Is there some way that we could automatically instantiate assert P in the callers? Is there some subtle reason that this isn't always valid, or why they behave differently?

I've attached a concrete example below. Unfortunately it's quite complicated. I spent some time trying to reduce it but I couldn't simplify it more than this. The complexity is kind of inherent because it only starts to show up for non-trivial programs that Kind2 can't prove immediately.

Thanks for any advice or clues,
Amos

-- return true if 'x' has been true the last 'n' ticks
node lastn(x: bool; const n: int)
returns (out: bool)
var
  count: int;
  prev:  int;
let
  prev = 0 -> pre count;
  count = if x then (if prev = n then n else prev + 1) else 0;
  out = count = n;
tel

const ALPHA10   : int = 70; -- 70/1024 = 0.068359
const ALPHA_MAX : int = 1024;
const INT32_MAX:  int = 2147483647;

const EMA_RANGE : int = INT32_MAX / ALPHA_MAX;
type EMA_INPUT = subrange[0, EMA_RANGE] of int;

-- fixed-point exponential moving average
node ema10(x: EMA_INPUT) returns (y: EMA_INPUT)
var yp : int;
let
  yp = x -> pre y;
  y = (x - yp) * ALPHA10 / ALPHA_MAX + yp;
tel

const EPSILON : int = 100;
const TICKS : int = 10;

-- Check if exponential moving average is out of bounds, has abstract contract to hide details
node ema10_check(inp: EMA_INPUT) returns (ok: bool)
(*@contract
  guarantee lastn(inp > EPSILON * 20, TICKS) => not ok;
*)
var e10 : EMA_INPUT;
let
  e10 = ema10(inp);
  ok = e10 <= 2 * EPSILON;
tel

-- Just some filter on the input signal so that the example is not completely trivial
function filter_input(i : int)
returns (e : EMA_INPUT)
let
  e = if i < 0 then 0 else if i / 2 > EMA_RANGE then EMA_RANGE else i / 2;
tel

node ema10_check2(
  inp1, inp2: EMA_INPUT
) returns (
  ok: bool
)
let
  ok = ema10_check(filter_input(inp1))
   and ema10_check(filter_input(inp2));

  -- These properties are basically the same as the guarantee on ema10_check, but just slightly different
  --%PROPERTY lastn(filter_input(inp1) > EPSILON * 20, TICKS) => not ok;
  --%PROPERTY lastn(filter_input(inp2) > EPSILON * 20, TICKS) => not ok;

  -- These assertions are the instantiated guarantees of ema10_check.
  -- Uncommenting these assertions lets Kind2 solve the above properties immediately.
  -- With the assertions commented out, Kind2 can't seem to prove it (times out after a minute)
  -- assert lastn(filter_input(inp1) > EPSILON * 20, TICKS) => not ema10_check(filter_input(inp1));
  -- assert lastn(filter_input(inp2) > EPSILON * 20, TICKS) => not ema10_check(filter_input(inp2));
tel

Answer 1 · 2021-04-06T05:42:11.000Z

Actually, I wonder whether this could be related to the new bounds checking: this particular example works fine with ~~an old version of Kind2 (from October last year)~~ [Kind2/develop from last week]. I forgot to mention that it requires composition and modular to be true (kind2 ema_test3.lus --modular true --compositional true --check_subproperties false).

Could it be that the new bounds checking is encoding the guarantee as something like bounds_ok(input) => P(input, output), and so it isn't immediately obvious that the guarantee P is true?

Answer 2 · 2021-04-06T18:15:03.000Z

Hi Amos. Thank you for reporting this issue. It is very helpful for understanding the limitations of Kind 2.

Could it be that the new bounds checking is encoding the guarantee as something like bounds_ok(input) => P(input, output), and so it isn't immediately obvious that the guarantee P is true?

I think that is the reason. We use always(bounds_ok(input)) => always(P(input, output)). As a test, you can try to replace the definition of EMA_INPUT with type EMA_INPUT = int and call Kind 2 using only compositional mode (not modular), and you will see that Kind 2 is able to prove the properties of ema10_check2.

Let's keep this issue open as a reminder that we need to study how to make the satisfaction of properties like these more obvious for Kind 2.

Answer 3 · 2021-04-07T16:52:49.000Z

Hi Amos,

Here is a remark for the particular example provided, just in case it helps for proving properties of your original models. The main reason why Kind 2 has troubles proving the properties is due to the presence of the integer division in filter_input. Sometimes, like in this case, it might help to provide a concrete axiomatization of the operator:

node imported idiv2(x: int) returns (q:int; r:int);
(*@contract
  -- Euclidean definition (semantics used by Kind 2)
  guarantee 0 <= r and r <= 1;
  guarantee x = 2*q + r;
*)

node idiv2_q(x: int) returns (q:int);
var r:int;
let
  q,r = idiv2(x);
tel

Then you can use it in this way:

node filter_input(i : int)
returns (e : EMA_INPUT)
let
  e = if i < 0 then 0 else if idiv2_q(i) > EMA_RANGE then EMA_RANGE else idiv2_q(i);
tel

I hope this is helpful.

Answer 4 · 2021-04-07T23:57:54.000Z

Hi Daniel,

Thanks for the trick about integer division. Unfortunately the original program doesn't have integer division for filter_input – I just used it as something complex enough for the example – but maybe I can add a simplified contract there as well.

At a higher level, do you think it would make sense to have some sort of preprocessing phase that marks as solved any local propositions that are (alpha-)equivalent to the instantiated guarantees of calls to nodes with contracts? I believe this is sound, since the use of the contract will still require the assumptions to be proved separately. It should also be predictable and well-defined (but quite weak).

This sort of 'solve by substitution' would help for our original case, as Kind2 can prove the assumptions of the call with contract fine, but when I add a local property that's the substitution of the guarantee that fails.

Do you think this preprocessing would be a reasonable approach? Do you think it would be very hard to implement? I'm happy to have a go if you think it's worth trying.

Answer 5 · 2021-04-14T03:52:20.000Z

Hi Amos,

I created a pull request (#739) that fixes this issue. When a call with a contract is abstracted with an implication like SoFar(assumptions) => guarantees in the verification problem, Kind 2 declares the antecedent invariant as soon as all the assumptions are proved invariant. This makes the consequent accessible immediately, which is enough (together some simple auxiliary invariants) to prove the properties in your example.

Please feel free to reopen the issue if you still experience problems with other models.

Thanks,
Daniel

Answer 6 · 2021-05-06T01:10:48.000Z

Thanks Daniel! Sorry I haven't had a chance to properly try this out yet, but it looks promising

Answer 7 · 2022-03-21T08:39:47.000Z

Hi Daniel,

I hope you don't mind me coming back to this issue after so long.

We've recently been having issues with contracts again. They usually work for smaller examples, but we're having trouble composing them together into larger models. We can usually prove the precondition OK at the use-site, but the postcondition will time out.

I've been going through a few artificial examples to better understand what's happening. I would consider the following one to be "definitionally true". Kind2 proves it fine if you have invariant generation enabled, but it won't go through if invariant generation is disabled. I think that if it were possible to prove contracts like these without invariant generation it'd be much more predictable and scalable - when the nodes get a bit bigger it's impossible to know whether the right invariants will be generated in time. (That's my impression as a user at least, not knowing the details of invariant generation.)

-- To test I ran with kind2 lus/lastn-twice.lus --disable IC3 --disable INVGEN --disable INVGENOS --disable INVGENREALOS --disable INVGENINTOS
node lastn(x: bool; const n: int)
returns (out: bool)
var
	count: int;
	prev:  int;
let
	prev = 0 -> pre count;
	count = if x then (if prev = n then n else prev + 1) else 0;
	out = count = n;
tel

node imported with_contract(x: bool; const n: int) returns (ok: bool)
(*@contract guarantee lastn(x, n) => ok; *)

node top(x: bool; const n: int) returns (top_ok: bool)
let
  top_ok = with_contract(x, n);
  --%PROPERTY lastn(x, n) => top_ok;
tel

Looking at the generated SMT problem, the main issue seems to be that the two different calls to lastn are completely separate instances. The call in the contract of with_contract is one instance, and the property of top is another instance with different state. There's no invariant linking the states of the two, and I can't write one manually because I can't refer to the internal state of lastn without changing the return types of both lastn and with_contract.

I was thinking that one option would be to inline the contract into the calling node as a property for the assumes and an unchecked assertion for the guarantees. That way the two calls to lastn would share the same instance, and so would not require many (any?) extra invariants to get it through.

This inlining and common subexpression elimination would be a bit surprising though, because the exact same contract and its definition would have slightly different behaviour. The CSE would also change the semantics if a contract referred to any non-deterministic functions, though that seems surprising to begin with.

What do you think?

Thanks for your time,
Amos

Answer 8 · 2022-03-22T02:25:49.000Z

Hi Amos,

Thank you for sharing your experience with us and raising this issue.

We are considering applying a more general solution to this problem. Namely, guide Kind 2 to discover behavioral equivalences between calls to a same node. We would like to try this before applying a more specific solution.

I'll keep you posted here on any progress.

Best regards,
Daniel

Answer 9 · 2022-04-01T04:36:09.000Z

Hi Amos,

PR #877 provides a tentative solution to this issue.

I would appreciate it if you could test this change with your models, and let me know how well it works.

Thanks,
Daniel

Answer 10 · 2022-04-01T07:47:11.000Z

Hi Daniel,

Thanks for the quick solution. I just had a quick look and it sounds promising but I'll try it out properly sometime this weekend.

Amos

Answer 11 · 2022-04-04T09:55:00.000Z

Hi Daniel,
I can't give a concrete answer yet as I'm still working through trying this on our models, but it is definitely an improvement in some cases and I haven't seen any regressions.

When trying this out I did have an issue: I had a contract guarantee P => Q, but what I really want to prove is P => R. If I state P => Q as a property it goes through in <2s, and if I state Q => R separately then it goes through instantly. But if I state both of them, it gets Q => R instantly but the contract P => Q won't go through even after a minute. I see the same behaviour if I replace Q => R with R or not R.

R transitively depends on a pure function with a contract. When I don't mention R in a property the occurrence of that function can be removed by slicing, so perhaps that's why it works without these properties. For some reason I can get it to go through by removing the contract from the function, even though the contract is simpler than the implementation. Interestingly, if I replace the contract with a guarantee that states the body of the function it still will not go through, which suggests to me that something is strange with contracts on functions. This isn't related to your PR #877 - I have the same issue with an older version of Kind2.

Thanks for all your help. I will keep trying to create a smallish example and let you know how I go.
Amos

Answer 12 · 2022-04-04T14:45:53.000Z

Hi Amos,

Thank you for the update.

When a component is declared as a function (as opposed to a node), Kind 2 makes the commitment of treating the component as a true mathematical function. That is, given the same input(s) the function provides the same output(s) at all times. This is similar to what PR #877 is aiming to achieve for nodes, but the approach used for functions is different and the provided guarantees are stronger. The consequence of this additional constraint is that reasoning about a model in presence of imported functions or functions abstracted by their contracts is a lot harder for Kind 2 (this is not the case when a full implementation for a function is available and the current analysis uses it because the definition of the function ensures the satisfaction of the requirement). Moreover, the current IC3 engine cannot work with these systems and is automatically disabled.

We have plans to improve the support of abstracted functions in the future, but until that happens there exists a workaround you can try. You can declare the function as a node which will avoid adding the additional constraint. If the contract of the function (together the rest of guarantees) is strong enough to prove the properties of the caller, the verification will go through and you do not have to worry about anything else. If the contract of the function is not strong enough, you may get a spurious counterexample that does not respect the functional constraint. However, when compositional and modular analyses are enabled, Kind 2 will refine the function and use the implementation of the function in a new analysis to confirm or discard the counterexample.

I hope this helps.

Daniel

Answer 13 · 2022-04-05T23:47:45.000Z

That's very helpful - thanks Daniel. With this information about function contracts and PR #877 I think we will have a predictable way to compose proofs together. I will keep trying with our models but unfortunately I might not get a chance until this coming weekend. I'll let you know how we go.

Answer 14 · 2022-04-06T22:21:36.000Z

Hi Amos,

Thank you for your feedback.

FYI, we decided to make the functional constraint optional. PR #881 makes Kind 2 only enforce the constraint on abstract functions when a new flag, --enforce_func_congruence, is true (its default value is false). With this change, you will not need to re-declare your functions as nodes in your models, and Kind 2 will be able to keep detecting issues like references to previous values in the contract or the body of a function.

Hope this helps.

Daniel