## Stream: Coq users

### Topic: Trying to write specification of function (VST)

#### Lessness (Aug 02 2023 at 23:52):

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.

#### Paolo Giarrusso (Aug 03 2023 at 01:26):

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>

#### Michael Soegtrop (Aug 03 2023 at 07:28):

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

#### Michael Soegtrop (Aug 03 2023 at 07:30):

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

#### Notification Bot (Aug 04 2023 at 14:32):

Lessness has marked this topic as unresolved.

#### Lessness (Aug 04 2023 at 14:40):

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

#### Lessness (Aug 04 2023 at 16:02):

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?

#### Lessness (Aug 05 2023 at 10:53):

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.

#### Lessness (Aug 05 2023 at 11:31):

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

#### Lessness (Aug 05 2023 at 11:35):

Nah, still the same problem with `factorize`. :(

#### Paolo Giarrusso (Aug 05 2023 at 12:24):

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

#### Paolo Giarrusso (Aug 05 2023 at 12:30):

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

#### Paolo Giarrusso (Aug 05 2023 at 13:42):

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

#### Paolo Giarrusso (Aug 05 2023 at 14:57):

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.

#### Paolo Giarrusso (Aug 05 2023 at 14:59):

@Michael Soegtrop Have you seen docs for `GLOBALS (gv)` before? Should the manual be updated?

#### Lessness (Aug 05 2023 at 15:39):

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.

#### Paolo Giarrusso (Aug 05 2023 at 15:44):

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

#### Paolo Giarrusso (Aug 05 2023 at 15:44):

_and_ you need `GLOBALS (gv)` in the spec

Thank you!

#### Paolo Giarrusso (Aug 05 2023 at 15:47):

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