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?

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. :)

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.

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.

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 ()).
```

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 `admit`

s. 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.

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

Lessness has marked this topic as resolved.

Last updated: Jun 15 2024 at 23:01 UTC