Stream: Coq users

Topic: ✔ Difficulties verifying simple C program

Lessness (Aug 06 2021 at 18:49):

Here's github repository: https://github.com/LessnessRandomness/PE
EulerProject1.c is the C program, EulerProject1.v is result of clightgen.exe processing, Verif_EulerProject1.v is where I try to verify everything.

I am stuck trying to prove that function main fulfills the specification. This is goal I have.

1 subgoal
Espec : OracleKind
gv : globals
Delta_specs : PTree.t funspec
______________________________________(1/1)
has_ext tt |-- emp

There are many possibilities for me do something wrong because I'm beginner and don't understand exactly what I'm doing here.
Big thanks for any hints!

Lessness (Aug 08 2021 at 21:59):

I made a tiny change in the specification of main function: changed SEP() to SEP(TT).

Definition main_spec :=
 DECLARE _main
  WITH gv : globals
  PRE  [] main_pre prog tt gv
  POST [ tint ]
     PROP()
     RETURN (Vint (Int.repr (result 999)))
     SEP(TT).

Then forward tactic did its job (after some time) and proof of the lemma body_main was successfully finished.

Notification Bot (Aug 09 2021 at 16:12):

Lessness has marked this topic as resolved.

Ben Siraphob (Aug 15 2021 at 18:36):

@Lessness that's strange, I guess I need to learn more about separation logic to know when to use TT

Lessness (Aug 16 2021 at 11:30):

I took it from Verif_sumarray.v chapter, without any understanding.

Notification Bot (Aug 27 2021 at 23:19):

Lessness has marked this topic as unresolved.

Lessness (Aug 27 2021 at 23:23):

Apologies for the necromancy.

The issue is that the last forward takes so much time (at least on my computer). I ran time forward and it gave time equal to more than 13 minutes. Is there a way of making it faster?

Lessness (Aug 27 2021 at 23:34):

Yes, there is a way.

Lemma body_main: semax_body Vprog Gprog f_main main_spec.
Proof.
  start_function. forward_call 999.
  + lia.
  + remember (result 999) as W. clear HeqW. time forward.
Qed.

This results in less than 4 seconds of waiting time. I speculate that the result 999 somehow has to be calculated (if true then why?) and that, of course, takes time.

Paolo Giarrusso (Aug 27 2021 at 23:42):

How long does simpl take on result 999, and how big is the result? Generally, if some computation is expensive, in Coq it’s up to you to prevent the expensive computation.

Paolo Giarrusso (Aug 27 2021 at 23:44):

note I haven’t used VST specifically, but some automation tactics will likely want to call simpl (and/or cbn) at some point.

Lessness (Aug 27 2021 at 23:44):

Eval simpl in (result 999) is immediate - it returns the same result 999.

Lessness (Aug 27 2021 at 23:47):

Though Eval cbn in (result 999)is not and, probably, will take the same >13 minutes.

Paolo Giarrusso (Aug 27 2021 at 23:47):

oh I see, you’d likely have to unfold result for it to reduce; but there’s lots of things that can trigger reduction.

Paolo Giarrusso (Aug 27 2021 at 23:48):

or partial reduction. And if some intermediate step is a big term, its presence in your goal/context might make _other_ tactics slower.

Paolo Giarrusso (Aug 27 2021 at 23:49):

bad remedy: Opaque result. That will block reduction of result in many cases, except a few ones (due to bugs) and a few others (which are not bugs; it’d be unsound for Opaque to disable definitional equality).

Paolo Giarrusso (Aug 27 2021 at 23:50):

one solution is ssreflect’s lock mechanism, _but_ I wouldn’t know how well ssrelect and VST play together.

Paolo Giarrusso (Aug 27 2021 at 23:50):

I use stdpp’s sealing, but I also don’t know how well stdpp and VST play together.

Lessness (Aug 27 2021 at 23:53):

I like my remember (result 999) as W. clear HeqW. method the most.

And Opaque result is not helping. :(

Lessness (Aug 27 2021 at 23:54):

Oh, Opaque result is helping a bit. Now forward command lasted 70 seconds.

Lessness (Aug 28 2021 at 00:03):

I speculate, again, that it is some kind of bug or inefficiency in VST, because result 999 should not be reduced or anything to prove the lemma body_main. Or else the remember (result 999) as W. clear HeqW. method wouldn't make forward command so fast.

Paolo Giarrusso (Aug 28 2021 at 00:10):

Sure, but how is VST supposed to know that?

Paolo Giarrusso (Aug 28 2021 at 00:11):

it's not going to try whether to reduce each possible subterm or not.

Paolo Giarrusso (Aug 28 2021 at 00:12):

however, many Coq commands can trigger reduction: say, applying a lemma uses unification to match the lemma conclusion with your goal, which sometimes involves reduction.

Paolo Giarrusso (Aug 28 2021 at 00:13):

and such unification depends on lots of hard-to-predict heuristics.

Lessness (Aug 28 2021 at 00:16):

Yes, that makes sense. Thank you!

Notification Bot (Aug 28 2021 at 00:22):

Lessness has marked this topic as resolved.

Paolo Giarrusso (Aug 28 2021 at 05:58):

(Again, I have not studied VST internals, but e.g. CPDT does not present ways to avoid that, _AFAIR_).

Last updated: Apr 19 2024 at 23:02 UTC