SF Vol5Beta Verifiable C - Dealing with if · Coq users

The issue that I'm stuck on I think is just specific to Verifiable C's syntax etc, vs some deep Software Foundations specific issue.

semax Delta
  (PROP ( )
   LOCAL (temp _q vret; temp _p p; temp _i (Vint (Int.repr i));
   gvars gv)
   SEP (mem_mgr gv;
   if eq_dec vret nullval
   then emp
   else
    malloc_token Ews (Tstruct _cons noattr) vret *
    data_at_ Ews (Tstruct _cons noattr) vret; stack il p))
  (if (! _q) {
     _exit([((1))%expr]);
   }
   MORE_COMMANDS) POSTCONDITION

Intuitively, this doesn't seem to complicated...but up to now, the module doesn't explain how to deal with if statements, and the syntax of local pre/postconditions is hazy. I've spent a little time with the more detailed docks from Verifiable C and don't see an answer, though I'll read them more thoroughly next.

Regardless, my thought was first to destruct (eq_dec vret nullval)...In the case where vret=nullval, we have LOCAL (temp _q nullval) as a local predicate, which means that we know it will exit. In the other case, we know vert <> nullval which means that _q <> nullval. I've tried various things, but I'm just not sure how to connect these pieces of information together. forward_if requires a proposition, but it's unclear what that should be. Stuff like assert_PROP (_q = nullval) doesn't typecheck.

A general thought is perhaps the postcondition to use with forward_if is something that says "temp _q in fact is the value we think".

I feel like I'm missing something fairly obvious, I just am still getting used to connecting the pieces... appreciate any guidance.

jco (Jul 03 2020 at 14:52):

Of course right as I posted this I realized I could do forward_if (SEP (data_at_ Ews (Tstruct _cons noattr) vret))...which has given me some progress, though the rest of my handling is a bit ugly, so I'm not sure if that is the right route to take or not. If it is...argh, why is it always that right as we ask the question we figure it out? Regardless, I welcome any tips for dealing with this sort of thing in veriable c! It's a super cool system, but I feel like it's key to sort of learn an alternate "verifiable c language".

jco (Jul 03 2020 at 15:01):

So having used that forward_if statement I made some progress, but eventually hit another wall...so I think the issue is that I'm not super clear on 1. entailment and 2. the sorts of assertions that forward_if works with.

ENTAIL Delta,
PROP ( )
LOCAL (temp _q vret; temp _p p; temp _i (Vint (Int.repr i));
gvars gv)
SEP (mem_mgr gv;
malloc_token Ews (Tstruct _cons noattr) vret *
data_at_ Ews (Tstruct _cons noattr) vret; stack il p)
|-- SEP (data_at_ Ews (Tstruct _cons noattr) vret)

Tactic failure: The right hand side is messed up; perhaps you inadvertently did something like 'simpl in *' that changes POSTCONDITION into a form that Floyd cannot recognize.  You may do 'unfold abbreviate in POSTCONDITION' in your previous proof steps to inspect it (level 998).

This makes me think that the issue is that while I had the right general idea, my postcondition was not expressed correctly.

I should spend some time better understanding entailment and what form of things it expects....

jco (Jul 03 2020 at 15:08):

I think the postcondition of forward_if needs to include _q and needs to be about the fact that if the malloc succeeds, then we have an actual stack. I guess I should figure out what makes sense, type wise...

Simon Hudon (Jul 03 2020 at 15:44):

I've been trying to start using VST. You gave me the idea of starting with SF Vol5. I'll have to catch up before I can say anything useful though

jco (Jul 03 2020 at 16:45):

@Simon Hudon it's super super super cool. But def have to sort of learn a proof and tactic ecosystem

Stream: Coq users

Topic: SF Vol5Beta Verifiable C - Dealing with if

jco (Jul 03 2020 at 14:44):

jco (Jul 03 2020 at 14:52):

jco (Jul 03 2020 at 15:01):

jco (Jul 03 2020 at 15:08):

Simon Hudon (Jul 03 2020 at 15:44):

jco (Jul 03 2020 at 16:45):