[CN] Add inlined predicate assertions

[scuellar]

CN version 86abdf5d5468b543f2e1e73282240c8d7e5a9a54.

Assertions are a powerful tool for debugging verification scripts by

1. checking assertions at a point in the control flow and
2. ensuring the condition is added to the context.

CN has limited supports for inline assertions such as assert(false) but it cannot support more things like assert (Owned<struct int>(r)). However, the functionality is mostly present since we can encode assertions as a trivial lemma

/*@
  lemma assert_own (pointer p)
  requires take x0 = Owned<struct int_pair>(p);
  ensures  take x1 = Owned<struct int_pair>(p);
@*/

Then the assertions can be inlined with /*@ apply assert_own(ret); @*/. The lemma workaround satisfies 1 and 2 above. However writing a lemma for each assertion is tedious when debugging real programs.

An ideal solution would be to provide an assertion keyword for general predicates in CN that would also capture local variables, so we don't have to write generic lemmas/predicates. I would also venture to guess that these assertions will be the right hook to do property based testing (@bcpierce00 is this how you are thinking about it?).

[bcpierce00]

An ideal solution would be to provide an assertion keyword for general predicates in CN that would also capture local variables, so we don't have to write generic lemmas/predicates. I would also venture to guess that these assertions will be the right hook to do property based testing ( @bcpierce00 https://urldefense.com/v3/__https://github.com/bcpierce00__;!!IBzWLUs!Vh9V0PwCRdi7SFp4Nxk0PMYayJlZsrmVVyN3AoFpzfIdzFyoQuDH8p3JahJ0rbBFfwLxQ4FFvIq92O3hHjTm1jzx7LMl$ is this how you are thinking about it?).

We haven't really gotten to this level of detail yet, but our first step would be to deal just with pre-/post-conditions (i.e., generate a heap state satisfying the precondition, run the function, check the postcondition). However, this kind of intermediate checkpoints could help fail faster. I imagine Rini might also be able to use them?

Message ID: @.***>

[septract]

Here's an example of @scuellar's encoding in use:

// Assert and prove a property about memory cells. Uses the lemma-hack way of
// asserting memory properties 

/*@
  lemma assert_own (pointer p)
  requires take x0 = Owned<int>(p);
  ensures  
    take x1 = Owned<int>(p);
    x1 == x0; // <-- Note, otherwise the lemma havocs the memory contents 
@*/

void assert_3(int *x, int *y)
/*@ requires 
      take Xpre = Owned<int>(x); 
      take Ypre = Owned<int>(y);
      *x == 7i32; *y == 7i32; @*/
/*@ ensures 
      take Xpost = Owned<int>(x);
      take Ypost = Owned<int>(y);
      *x == 0i32; *y == 0i32; @*/
{
  *x = 0;
  assert(*x == 0 && *y == 7);
  /*@ apply assert_own(x); @*/
  /*@ apply assert_own(y); @*/
  assert(*x == 0 && *y == 7);
  *y = 0;
  assert(*x == 0 && *y == 0);
}

BTW the following variant does not parse:

  /*@ apply assert_own(x); assert_own(y); @*/