Here is all the tiny C code:

```
// https://codereview.stackexchange.com/a/74792 by Alnitak
#include <stddef.h>
#include <stdint.h>
uint64_t highest;
// checks if `f` is a factor of `n`,
// returning divided `n` accordingly
uint64_t factorize(uint64_t n, uint64_t f) {
if (n < f) return n;
while (n % f == 0) {
n /= f;
if (f > highest) {
highest = f;
}
}
return n;
}
uint64_t find(uint64_t n) {
highest = 1;
// check the two simplest cases
n = factorize(n, 2);
n = factorize(n, 3);
// and then all numbers in the form 6x - 1 and 6x + 1
if (n >= 5) {
for (uint64_t i = 5; i * i <= n; i += 6) {
n = factorize(n, i);
n = factorize(n, i + 2);
}
}
return (n == 1) ? highest : n;
}
int main(void) {
return find(600851475143);
}
```

I'm trying to write the specification for the function `factorize`

but I don't understand yet how and where to put the claim that the function looks at the value of `highest`

and, depending on it and values of `n`

and `f`

, modifies it.

Here the current state of the specification:

```
Definition factorize_spec: ident * funspec :=
DECLARE _factorize
WITH gv: globals, n: Z, f: Z
PRE [ tulong, tulong ]
PROP(2 <= n <= Int64.max_signed; 2 <= f <= Int64.max_unsigned)
PARAMS(Vlong (Int64.repr n); Vlong (Int64.repr f))
SEP()
POST [ tulong ]
PROP()
RETURN(Vlong (Int64.repr (repeated_div f n)))
SEP().
```

Any hints how to finish it? Thanks in advance.

I haven't used VST specifically, but In separation logic, I'd expect you should pass in *ownership* of highest via a points-to predicate: in the precondition, &highest points to some value h, and in the postcondition it points to <some function of h, n and f>

@Lessness : I really recommend you to go through the lecture material Andrew prepared for VST: https://softwarefoundations.cis.upenn.edu/vc-current/index.html.

Writing the spec is very likely the least problem you will have on the road of using VST und the course material is an excellent preparation. Going through the material without the VSU part should take you less than a week if you do all exercises (which I would recommend).

And I am quite sure that going through the material will save you much more than one week of time later.

Lessness has marked this topic as unresolved.

So, here is the .v file where I try to prove that the function `factorize`

satisfies the specification: https://github.com/LessnessRandomness/PE/blob/main/Verif_EulerProject3.v

And the file with clightgen output for the tiny C program:

https://github.com/LessnessRandomness/PE/blob/main/EulerProject3.v

Do I have the correct loop invariant (at the end of `Verif_EulerProject3.v`

? If someone has free time to take a look, I would be thankful.

(While I'm stuck with this I will read/learn further from the Software Foundations Verifiable C book.)

Trying to prove theorem `factorize_result`

there is a moment when `forward`

tactic fails with:

`Tactic failure: Cannot evaluate right-hand-side expression (sometimes this is caused by missing LOCALs in your precondition) (level 995).`

So maybe my specification `factorize_spec`

is missing something?

Simplified the problem. See the test.c, test.v and Verif_test.v in https://github.com/LessnessRandomness/PE/

So, it's clear now I don't know how to write correct specification when there're some global variables.

If I write specification for this tiny C function successfully, I will know how to fix the specification of `factorize`

too.

Adding line `GLOBALS (gv)`

fixed my difficulties with get_counter function:

```
Definition get_counter_spec: ident * funspec :=
DECLARE _get_counter
WITH gv: globals, c: Z
PRE []
PROP (0 <= c <= 100)
PARAMS ()
GLOBALS (gv)
SEP (data_at Ews tint (Vint (Int.repr c)) (gv _COUNTER))
POST [ tint ]
PROP ()
RETURN (Vint (Int.repr (c + 1)))
SEP (data_at Ews tint (Vint (Int.repr (c + 1))) (gv _COUNTER)).
```

Nah, still the same problem with `factorize`

. :(

hmm

```
$ coqc Verif_test.v
File "./Verif_test.v", line 1, characters 0-35:
Error: Cannot find a physical path bound to logical path VST.floyd.proofauto.
$ opam list|grep vst
coq-vst 2.11 Verified Software Toolchain
coq-vst-zlist 2.11 A list library indexed by Z type, with a powerful automatic solver
```

oh, weird, vst is only installed in `/Users/pgiarrusso1/.opam/__coq-platform.2022.09.0~8.16.0~2022.09~beta1/lib/coq-variant/VST_aarch64_64`

in `__coq-platform.2022.09.0~8.16.0~2022.09~beta1`

on Apple Silicon cc @Michael Soegtrop ? I'll troubleshoot locally a bit

okay, setup problem fixed with `-Q /Users/pgiarrusso1/.opam/__coq-platform.2022.09.0~8.16.0~2022.09~beta1/lib/coq-variant/VST_aarch64_64/VST VST`

.

I managed to verify this. Turns out the spec needs `GLOBALS (gv)`

, but I have _not_ found documentation for this — I read https://github.com/PrincetonUniversity/VST/blob/288866356f56222be47af66630602e5cc0e14490/floyd/canon.v instead, and I have no idea not sure why `GLOBALS`

takes a list.

The reference https://vst.cs.princeton.edu/download/VC.pdf mentions `LOCAL (gvars gv) — that gave me parse errors until I added `

Require Import VST.floyd.Funspec_old_Notation.` and dropped `

PARAMS ()`.

Complete code in https://github.com/LessnessRandomness/PE/pull/1; I also added necessary side conditions to verify the arithmetic, based on my experience with C and on (EDIT) skimming the intro of the SF volume.

@Michael Soegtrop Have you seen docs for `GLOBALS (gv)`

before? Should the manual be updated?

Thank you very much!

Will try to fix my `factorize`

spec proof.

Though here `GLOBALS (gv)`

seems not helping, but I will try to fix it myself somehow.

`forward_while`

needs `LOCAL (temp _n (Vlong (Int64.repr n)); temp _f (Vlong (Int64.repr f)); gvars gv)`

_and_ you need `GLOBALS (gv)`

in the spec

Thank you!

rationale/debugging hint: when you call `forward_while`

, the goal has `LOCAL (gvars gv)`

:

```
semax Delta
(PROP ( )
LOCAL (gvars gv; temp _n (Vlong (Int64.repr n));
temp _f (Vlong (Int64.repr f)))
SEP (data_at Ews tulong (Vlong (Int64.repr h)) (gv _highest)))
(while (_n % _f == (0)) {
LOOP_BODY
}
MORE_COMMANDS) POSTCONDITION
```

and that construct also appears in old-style specs. But `forward_while`

gives something like "a spec for the loop", and what's not mentioned in that spec is not available.

Last updated: Jun 13 2024 at 19:02 UTC