Stream: Coq users

Topic: ✔ Need help with "forward_while" command (Verifiable C, VST)

Lessness (Aug 16 2021 at 14:31):

As previously, the files are here: C source file - https://github.com/LessnessRandomness/PE/blob/main/EulerProject2.c , result of clightgen.exe - https://github.com/LessnessRandomness/PE/blob/main/EulerProject2.v and file where I do formalisation and verifying - https://github.com/LessnessRandomness/PE/blob/main/Verif_EulerProject2.v

I'm stuck proving lemma body_main... as I don't understand properly how to define loop invariant and stuff for forward_while command.
Can someone help?

Lessness (Aug 19 2021 at 19:57):

Frustrated noises... I don't get why it isn't working etc. Where I'm making a mistake...

I'm going understand all this sooner or later. And then one option is to write some tutorial for noobs like me. :)

Lessness (Aug 23 2021 at 14:58):

Changed loop invariant (in the forward_while command) to

forward_while (EX i: nat,
    PROP (0 <= even_fib i <= 5000000)
    LOCAL (temp _a (Vint (Int.repr (match i with O => 0 | S n => even_fib n end)));
           temp _b (Vint (Int.repr (even_fib i)));
           temp _result (Vint (Int.repr (sum_Z (map even_fib (seq 0 i))))))
    SEP (TT)).

and it worked.

It seems that I have some misunderstanding about loop invariants, though. I want to skip the last iteration or smth like that.

Paolo Giarrusso (Aug 26 2021 at 03:41):

You might already know, but the loop invariant even holds after the last iteration, only the condition changes:
https://en.wikipedia.org/wiki/Loop_invariant#Floyd%E2%80%93Hoare_logic.

Lessness (Aug 31 2021 at 09:10):

What kind of loop invariant would you choose here?

unsigned int result(unsigned int max) {
    unsigned int a, b, t, sum;
    sum = 0;
    a = 0;
    b = 2;
    while (b <= max) {
        sum += b;
        t = a;
        a = b;
        b = 4 * a + t;
    }
    return sum;
}

More specifically, what would you write instead of question marks? (M is, of course, bigger than 1. Even_fibonacci_efficient is function for calculating consecutive even Fibonacci numbers: 2, 8, 34, 144, etc.)

    forward_while (EX i: nat,
      PROP ( ??????? )
      LOCAL (temp _max (Vint (Int.repr M));
             temp _a (Vint (Int.repr (match i with O => 0 | S n => even_fibonacci_efficient n end)));
             temp _b (Vint (Int.repr (even_fibonacci_efficient i)));
             temp _sum (Vint (Int.repr (result_simple (match i with O => 0 | S n => even_fibonacci_efficient n end)))))
      SEP ()).

Lessness (Aug 31 2021 at 14:38):

https://github.com/LessnessRandomness/PE/blob/main/Verif_EulerProject2.v contains what I have achieved for now. (The C file and corresponding clightgen.exe result is there, too, in the repository.)

The proof of lemma "body_result" still contains two holes or admits. But I believe that the loop invariants are correct and I just need some rest and inspiration to finish it. :) Or not, if I find any counterexamples which invalidates the holes I want to prove. That would be nice too, in some way.

Lessness (Aug 31 2021 at 15:03):

Yesss, I did it. Second Project Euler exercise is done. ^^

Notification Bot (Aug 31 2021 at 15:14):

Lessness has marked this topic as resolved.

Last updated: Apr 19 2024 at 11:02 UTC