[wp] non-provable local typing constraints in lemmas

Hi Jens,

This additional condition is related to the typing of C integers. It is not specific to Coq output. Suppose you have the following lemma:

lemma foo: \forall unsigned *p; 0 <= p ;

It translates to forall m: array addr int, p: addr. is_uint32 m[p] -> 0 <= m[p] ; removing the guard over m[p] would be incorrect and can introduce contradictions (false) in the system. The same kind of constraints apply to logic functions and (inductive) predicates.

Usually, these typing constraints are automatically added by WP when you access memory from the Code. I must go into your specific example to understand why it might not be the case…

@blanchard @bobot @baudin I'm afraid that, to fix the problem, we need to split the Typed memory model and spread the different kind of integers into different chunks. Then, we can have a global typing invariant on memory locations, as follows:

predicate is_uint32_m (m : array addr int) = forall p. is_uint32 m[p]

When translating C-code, we can add all these global invariants on memories into the proof context, not only on accessed values through pointers, which is the current behaviour of WP.

goal foo: forall m : array addr int, p : addr. is_uint32_m m -> 0 <= m[p]

and the side condition is_uint32_m m would be much easier to discharge from the proof context. This is, however, a major refactoring of the Typed memory model.

I guess that splitting the Typed memory model is a major piece of work. For my limited purposes, it would be sufficient if the VC are the 'same' as in Frama-C 20.

The difference comes from a fix that was introduced to solve a soundness problem, and I'm a bit anxious to revert it. The problem is that the generated formula can be unsound and may introduce a contradiction in the context, although in this example it seems to be ok

However, I'm also looking for a simpler solution to this problem…

Thanks for the explication!

Interestingly, the condition ((is_sint32 x_1)), where x1 refers to an array object wasn't there in Frama-C 20.

I also wonder whether this is related to this BTS issue: https://bts.frama-c.com/view.php?id=2332

Yes indeed, it is clearly related. In the current memory model, we don't have the typing information for C-integers since they are all merged into an array map addr int to unbound integers. To fix it, we need to move the typing constraints more globally.

I have a quick and dirty workaround for the short-term, which is to completely erase side conditions regarding C-types when generating lemmas, under user control:

add option -wp-weak-int-model, which would be documented as unsafe;
when this option is turned on, you loose all side-conditions like is_xxxx();
this is unsafe because, eg. you can prove a lemma such as \exists char c; c > 1000;
misusage is limited, because those side-conditions are only erased for user defined lemmas;
however, the user must convince himself that his lemma does not take advantage from integral ranges.

@allan @jens What do you think about this proposal?

(remark: the coq script for FC 20 then works for FC 21 up with only a small change in the intros)

I would definitely try it. Currently, we are in maintenance mode which means that we are not actively adding new lemmas. In other words, the risk of accidentally misusing this workaround should be small.

I do not have a better idea.

Ok let's do it!

Good. Please, tell me when it's available in the public repository.

changed the description

changed title from Coq question for Frama-C (public git version) to [wp] non-provable local typing constraints in lemmas

changed the description

added wp label

I have noticed that the -wp-weak-int-model option is available in the beta release. I have already adapted one proof which was easy and will continue with this. Thanks a lot! I will keep you informed.

Oh yes, too many things to do and I just forgot to warn you about this! But you have sphinx eyes…

Just be careful and not add this option on all your proofs, since it might introduce inconsistencies.

Although, please consider giving -wp-smoke-tests a try if you time to do so. This can take some time since most smoke tests are timeouts in the normal case. However, it might be helpful for detecting inconsistencies from axioms and/or lemmas.

What do you mean by not adding this option on all proofs ? I have added -wp-weak-int-model as one of several options to Frama-C.

I will also have a look at -wp-smoke-tests, however, as of now we do not have any axioms anymore in ACSL by Example.

Ok that's fine since I think you never use C-integer ranges at all in ACSL by Example...

I think I am now through with "converting" my coq proofs to the new options. For the most part the conversation was not difficult.

Nevertheless, there are a handful of proofs, where I got stuck. I will look at it closer in the coming days.

Working on the update of the WP tutorial, I discovered that this bug can cause trouble for programs that just needs the axioms to be provable. For example, in the following code, it is impossible to prove the post-condition of the function:

/*@ // Note: I removed the case when there is an element to count
  axiomatic Occurrences_Axiomatic{
    logic integer l_occurrences_of{L}(int value, int* in, integer from, integer to)
      reads in[from .. to-1];

    axiom occurrences_empty_range{L}:
    \forall int v, int* in, integer from, to;
      from >= to ==> l_occurrences_of{L}(v, in, from, to) == 0;

    axiom occurrences_positive_range_without_element{L}:
    \forall int v, int* in, integer from, to;
      (from < to && in[to-1] != v) ==>
        l_occurrences_of(v,in,from,to) == l_occurrences_of(v,in,from,to-1);
  }
*/
/*@ 
  requires beg < end <= 1000 ;
  ensures 
  \forall int v ;
    v != a[end-1] ==> 
      l_occurrences_of(v, a, beg, end) == 
      l_occurrences_of(v, a, beg, end-1);
*/
void l_occurrences_of_add_last(int* a, unsigned beg, unsigned end){}

Basically, by using the TIP to manually instantiate occurrences_positive_range_without_element on the goal, we get a proof obligation like:

Let x_1 = « a[x_0] »@L1.
Assume {
  (* Heap *)
  Type: region(a@L1.base) <= 0.
  (* Instance *)
  Have: (is_sint32(x_1) -> (x_2 = x_3)).
}
Prove: x_2 = x_3.

I could use -wp-weak-int-model but for a complete program, it is not something we really want I guess. Could we be more selective? By just preventing the generation of these conditions in lemmas and axioms for example?

EDIT: Ok, found some fun workaround:

void l_occurrences_of_add_last(int* a, unsigned beg, unsigned end){
  int x = a[end-1];
}

forces the generation of the is_int(a[end-1]).

I wonder whether something like

  frama-c -wp  @lemma -wp-weak-int-model -wp-prop -then (* normal option for the remaining vc *)

would work...

Out of curiosity, how long would it take to implement a the solution outlined by Loïc "split the Typed memory model and spread the different kind of integers into different chunks" ?

Allan is currently working on a PoC for that, I think it is not that complicated and could be fixed in a very near future.

This should work, but you shall at least specify -wp-no-weak-int-model after the -then otherwise the option still applies.

Please tell me when there is a version that I should try.

Hello Jens, a new version of Frama-C Scandium is available.

In this version we have added the generation of the right constraints for the typed memory model, it is activated when -wp-rte is enabled. Thus you might want to:

remove -wp-weak-int-model
check that -wp-rte is always there for all your proofs

Basically, you will get the same proof obligations as you had at the beginning, except that now, you should have the right assumptions in the goal to complete your Coq proof. On the tutorial, adapting the proofs was quite easy, basically:

each memory variable now has type constraint assumption (thus an intros to update),
each use of a lemma/axiom that has type constraints on its memory variables generates subgoals for these memory variables and assumption or auto should do the job.

Thanks for the update I will try it as soon as possible. We use -wp-rte by default, so chances are good.

How do I get the new beta?

It looks like the file at https://git.frama-c.com/pub/frama-c/-/wikis/downloads/frama-c-21.0-beta-Scandium.tar.gz hasn't changed since the first release (at least the download has the same size ...)

Indeed, currently it is only available via the scandium branch (https://git.frama-c.com/pub/frama-c/-/tree/stable/scandium)

I checked out the stable/scandium branch and so far have fixed 13 coq proofs of ACSL by Example. So far I have encountered no issues. I keep you informed.

assigned to @blanchard and unassigned @lcorrenson

I have now worked through ACSl by Example.

many coq lemmas were easy to fix
one lemma that couldn't be verified for more than two years(!) with Coq can be now verified. I think this might close issue https://bts.frama-c.com/view.php?id=2332
There are quite a few lemmas and proof obligations that are not verified automatically anymore. In other words, I have still work to do.
There is also a lemma that uses C integers. I have to think about whether we still need this.

Thanks a lot for the quick implementation of the additional "chunks"!!

There are quite a few lemmas and proof obligations that are not verified automatically anymore.

If some of them seem to be pretty simple, do not hesitate to post them, maybe I missed something.

There is also a lemma that uses C integers. I have to think about whether we still need this.

Interesting, which one ?

closed

reopened

[wp] non-provable local typing constraints in lemmas

Steps to reproduce the issue

Expected behaviour

Actual behaviour

Fix ideas

Child items ...

Activity