**Frama-CI Bot**
(bd24cb20)
*
at
04 Feb 04:10
*

Merge branch 'feature/wp/why3-extra-config' into 'master'

*
... and
3 more commits
*

Oh, I did not realize that using something beyond plain Alt-Ergo is OK. Also, after cleaning the session, Alt-Ergo can prove a much simpler version for `nth_concat`

:

```
let rec lemma nth_concat (u v: list 'a) (k: int)
requires { 0 <= k < length u + length v }
variant { k }
ensures { nth (concat u v) k =
if k < length u then nth u k else nth v (k - length u) }
= if 0 < k && 0 < length u then nth_concat (tail u) v (k - 1)
```

I've proved `eq_repeat_concat`

as well.

What remains to be done is `nth_repeat`

which might be much more problematic. At least, in Isabelle/HOL it took about a page of a dense proof using induction and arithmetic. Is `nth_repeat`

used anywhere?

Also, what about the abstract function `repeat_box`

and associated axioms? Do we leave them unchanged?

These definitions

```
let rec lemma extensionality (u v: list 'a)
requires { vlist_eq u v }
variant { u }
ensures { u = v }
=
match u, v with
| Cons _ tlu, Cons _ tlv -> extensionality tlu tlv
| Nil, Nil -> ()
| _ -> ()
end
let rec lemma nth_concat (u v: list 'a) (k: int)
requires { 0 <= k < length u + length v }
variant { k }
ensures { nth (concat u v) k =
if k < length u then nth u k else nth v (Int.(-) k (length u)) }
=
match u with
| Nil ->
match v with
| Nil -> ()
| Cons _ tlv -> if k = 0 then () else nth_concat Nil tlv (k - 1)
end
| Cons _ l -> if k = 0 then () else nth_concat l v (k - 1)
end
```

are proved with Auto Level 3.

I defined functions `head`

and `tail`

(maybe, they can find their way into ACSL in a form of `\head`

and `\tail`

), used inductive definition of `nth`

and made some progress with lemma functions. However, I got stuck with converting axioms `nth_concat`

and `extensionality`

into lemmas (there are some more axioms to convert, but these two look pretty essential). As you can see (in the current merge request), simple properties of `vlist_eq`

can be easily demonstrated. But `extensionality`

requires induction, where I could not figure out how to carry it in Why3 properly. Any advice is appreciated.

**Frama-CI Bot**
(98caba53)
*
at
02 Feb 03:46
*

Merge branch 'update-headers' into 'master'

*
... and
25 more commits
*

**Frama-CI Bot**
(0ee289af)
*
at
01 Feb 03:46
*

Merge branch 'feature/ci/black' into 'master'

*
... and
5 more commits
*

Generally, when you need a proof by induction in Why3, the idea is to work with a lemma function. You can find an example here: https://why3.lri.fr/doc/syntaxref.html#module-cloning

Indeed, it was only for the sake of the example, in my actual use case the `dune-project`

is well-formed.
But I do not know what triggers the silent failure exactly since in the example I provided, using the actual `dune-project`

file instead of an empty one gives the exact same error.

Thank you for the information. At the moment some tests are failing due to Why3 warnings similar to the following:

`warning: axiom extensionality does not contain any local abstract symbol (contains: (=), list, vlist_eq)`

In the updated reading, the axiom lists only non-abstract functions. On the other hand, proving it requires induction that does not work out of the box with the SMT solver. I believe the strategy mentioned earlier addresses this issue. What should I do to turn the axiom into a lemma and to prove it with plain Alt-Ergo?

You can use the test utility `./bin/test.sh`

to run individual tests. Just export the environment variables as explained by @blanchard above, and use `./bin/tests -p src/plugins/wp/tests/<path-to-individual-test>`

; you can find many tests in `tests/wp_plugin`

directory, more generally, find occurrences of `\list`

in the `*/.[ci]`

fiels. Cf. `./bin/tests.sh -h`

for more options.

This would be a good idea, however tests using lists are spread among different test directories.

Thank you for the details. Given that the change affects only `\list`

, would it make sense/be possible to run only tests that use this logic type?

WP tests that are impacted by your modification are what we called "qualification tests". For speed reasons, it uses a (versioned) cache that is currently not accessible out of our private GitLab (probably for no particular reasons, just that it was easier to put it there when we created this cache). Anyway, we could probably make it public, it just requires a bit of on our side.

In the meantime, I think that the following procedure should be enough for you so that you can execute all the tests. Just note that it might take quite *a lot* of time. First, you need to use `alt-ergo-free 2.2.0`

to rebuild the cache on your side. Then, create an empty directory somewhere to store the cache.
From a clear `master`

branch:

```
make
make run-ptests # creates the dune files of the tests
FRAMAC_WP_CACHEDIR=/absolute/path/to/the/cache/directory FRAMAC_WP_CACHE=update dune build -j<small level of parallelism> @src/plugins/wp/tests/ptests
```

This will build a cache of the test in you directory. It is a good idea to limit parallelism to minimize the chances of failure of the SMT solver. Once the cache is ready, you can work with your branch.

- using
`FRAMAC_WP_CACHE=offline`

, you disable the creation of new cache entries, it may be interesting to see which tests are impacted, - using
`FRAMAC_WP_CACHE=update`

, new cache entries are created, so you'll see new proof failures/success in tests results.

I've updated the source taking the comments into account:

- Isabelle/HOL theories have been removed
- lemmas relying on interactive proofs have been turned into axioms
- meta tags have been removed

Alt-Ergo is now sufficient to complete the proofs.

As to turning all axioms into lemmas/lemma functions that can be proved by Alt-Ergo, I can look into it if you provide some guidance/examples where I can learn the technique.

In any case, the current version is already much more powerful and can be used in inductive proofs.

As to the tests, I can see some specifications using `\list`

in `src/plugins/wp/tests`

and `README`

that tells to use `bin/test.sh`

, but I'm unsure whether these are the tests we are talking about and that they are sufficient.

**Frama-CI Bot**
(a3e88edb)
*
at
28 Jan 04:17
*

Merge branch 'fix/contributing' into 'master'

*
... and
21 more commits
*

Hi, thanks for contributing! We are actually on the way of sanitizing the Why3 librairies of WP and your proposal is very welcomed.

Although we are interesting into improving the interface between WP & Isabelle (Cf. our discussions in #2643), we are *not* planning to add Isabelle as a ground support for proving the WP why3 libraries. To comply with our continuous integration infrastructure, we currently need to stick to our reference SMT solver (currently Alt-Ergo) and to rely on Why3 lemma functions for inductive proofs.

The `meta`

could be registered *via* a Why3 plug-in. Although, for the WP-List module, it is OK to remove all of them. More precisely, it is OK to also remove the lemmas with this meta, although the associated functions shall receive a definition in turn. We actually plan to remove all to them.

As a driving direction, functions shall be given an implementation, with ACSL undefined behavior implemented by `any`

operators.
Axioms shall be turned into lemmas or lemma functions that can be proved by our reference SMT solver (we actually have a dedicated strategy inside Why3 IDE, that uses SMT solver and few tactics, eg. split-vc and inline-goal).
Hence, we don't want to have why3 sessions and proof scripts to be committed in the store (they are usually not reproducible across different computers).

The `repeat_box`

function allows for writing lemmas that are only applied at root instances of the `repeat`

operator. Otherwise, SMT solvers will instantiate lemmas eagerly until combinatorial blow up.

Running non-regression tests is a bit technical, I'll provide more information later.

Currently open questions:

- Why3 complains about tags
`meta "remove_for_" lemma ...`

because it does not understand the mark`"remove_for_"`

. To complete and check the proofs I commented out these lines and then uncommented them back. What should I do to let Why3 proceed with these meta tags? - As noted in the merge request description, two facts (
`nth_cons`

and`nth_concat`

) received a new premise`0 <= k`

. Is it OK? - The existence of
`repeat_box`

seems to be rather technical. Shall it be kept or replaced with a real definition? Shall the corresponding axioms be turned into lemmas? - The Why3 session and realizations with associated proof theories are included in the commit in the directory next to
`vlist.mlw`

. Is the location OK? - What regression tests should be used to check the new version?

This is a follow-up to the discussion from the Frama-C mailing list to bring standard inductive lists to Frama-C WP plugin.

Replaced an axiomatic definition of lists with the standard Why3 one:

- used standard Why3 list modules;
- replaced a declared list type with the standard one;
- provided definitions of all previously specified list functions except for
`repeat_box`

; - replaced all axioms with lemmas except for those related to
`repeat_box`

; - proved all new lemmas with Alt-Ergo and Isabelle/HOL;
- added Why3 session with Why3 realization files and associated Isabelle/HOL theories.

Facts `nth_cons`

and `nth_concat`

received a new premise for the index `0 <= k`

. All other facts have been kept intact.

Ok, I think we should fix it for 26.1.

It is mandatory since we are not specifying the name of the package.