Lessness (Aug 02 2023 at 23:52): 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 factorizebut 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)).
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
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
Lessness (Aug 05 2023 at 15:45):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: Oct 13 2024 at 01:02 UTC