why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2022-11-16T13:41:38+01:00https://gitlab.inria.fr/why3/why3/-/issues/711Recursion under quantifier inside of `let function`2022-11-16T13:41:38+01:00Xavier DenisRecursion under quantifier inside of `let function`I know that we discussed this back in october, but I cannot find any trace of our discussions.
Currently if you define a `let rec function` and perform a recursive call under a quantifier, you get an `unbound predicate or function` err...I know that we discussed this back in october, but I cannot find any trace of our discussions.
Currently if you define a `let rec function` and perform a recursive call under a quantifier, you get an `unbound predicate or function` error for namespace reasons.
We had discussed several solutions, but I forget what the tradeoffs were.
cc @x-DEwert who independently stumbled on this.https://gitlab.inria.fr/why3/why3/-/issues/591Misleading "unbound function" error message2021-09-27T14:23:59+02:00Xavier DenisMisleading "unbound function" error messageI was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel...I was recently caught by the error message:
`unbound function or predicate symbol 'UInt64.of_int'`
It took me a second to realize that the reason was being raised was that `of_int` is a `val` and not a `function` or `predicate`. I feel like the message could be improved when a program symbol with the same name appears, something like:
```
unbound function or predicate symbol 'UInt64.of_int', but a program symbol with the same name was found
```
Even this marginal improvement would make the error much more clear (imo).https://gitlab.inria.fr/why3/why3/-/issues/546Inductive proofs on inductives2021-02-11T10:35:12+01:00Loïc CorrensonInductive proofs on inductivesThis is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the ...This is a proposal feature allowing inductive proofs over inductive predicates in why3.
Consider an inductive predicate `P` as follows:
```
inductive p xs = A: forall ys. hs -> p es | ...
```
The idea is to automatically generate the following items:
- `type p'witness = A ys | ...` witnessing the universally quantified variables obtained to build a proof of `p` with each constructor
- `val ghost function p'proof xs : p'witness` returns, under precondition `p xs`, a witness of its (minimal) proof.
- `val ghost function p'induction xs : int` returns a (decreasing) variant over the proof of `p xs`.
The post condition of `p'proof xs` introduces, for each witness constructor `A ys` the hypotheses `hs` and the associated unifications of `es` and `xs`, together with strictly decreasing variants of `p'induction` for any sub-proofs of `p` in `hs`.
A complete example of how this can be used in practice is provided here:
- [ind.mlw](/uploads/a336611a3844c6a68dcbc8debfa44960/ind.mlw): full example of use of the generated symbols
(including also why3/why3#547 although it is not necessary…).
- [ind_gen.mlw](/uploads/d42763ecbdab345676b472d7d8fecdb6/ind_gen.mlw): the full exemple together with the (axiomatized) generated symbols, that makes the lemma proof automatically discharged easily.
- [ind.v](/uploads/042c16623daa356c4ef5ef0b792d3e06/ind.v): a Coq realization of the generated symbols of the example using destruction of the inductive predicate in `Type` (we can not realize modules... yet, although it shall look like this).
- [ind_fol.mlw](/uploads/dbf0d183aa20786db2437064782ba440/ind_fol.mlw): a fully proven Why-3 reference implementation (without inductives) for all the generated symbols of the example.https://gitlab.inria.fr/why3/why3/-/issues/508Detection of rsymbol that corresponds to a constant2023-06-22T16:46:36+02:00MARCHE ClaudeDetection of rsymbol that corresponds to a constantCurrently a declaration of the form
```
val constant x : int
```
is transformed into
```
let constant x : int { ensures result = x } = fun -> any int
```
This particular encoding should be taken into account both in extraction and execut...Currently a declaration of the form
```
val constant x : int
```
is transformed into
```
let constant x : int { ensures result = x } = fun -> any int
```
This particular encoding should be taken into account both in extraction and execution.
Feature wish : provide a new OCaml function that, given a rsymbol `rs`, and possibly the environment to access to its declaration, tells whether this rsymbol is a regular function or an encoding of a constant.Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/432Why3 uses too much memory2020-02-11T10:49:39+01:00Guillaume MelquiondWhy3 uses too much memoryThis is a meta-issue to summarize all the discussions into a single place.
Things to do:
- [X] Do not precompute `Decl.d_sysms`, as they consume about 15% memory.
- [x] Change `split_vc` so that it introduces premises by itself instead ...This is a meta-issue to summarize all the discussions into a single place.
Things to do:
- [X] Do not precompute `Decl.d_sysms`, as they consume about 15% memory.
- [x] Change `split_vc` so that it introduces premises by itself instead of relying on `introduce_premises`. The latter has too little information to share common declarations between subtasks. This should make the memory consumption linear rather than quadratic in the number of proof obligations.
- [ ] Investigate `Decl.known_add_decl`, as its `Mid.union` call seems responsible for about 25% memory consumption.
- [x] Investigate `Termcode.task_v3`, as its `Mid.add` call seems responsible for about 25% memory consumption.
Remark: The `master` branch supports memory profiling, when using a suitable compiler, e.g., the one from the Opam switch `4.07.1+statistical-memprof`. First, configure Why3 with `--enable-statmemprof` and build it. Then, execute `bin/why3ide -L examples/multiprecision examples/multiprecision/toom`. Once the interface is loaded, execute `sturgeon-connect` in Emacs to see the memory consumption. (See Statmemprof's documentation for details about Sturgeon.)https://gitlab.inria.fr/why3/why3/-/issues/400Improve shape structures2019-10-25T16:55:23+02:00Guillaume MelquiondImprove shape structuresAs explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in pr...As explained by @paskevyc in #276, the following could improve the situation with respect to the part of the shapes that is really needed for pairing:
"The idea is that a transformation that produces several tasks that only differ in premises (e.g., destruct or split_vc when the goal is no more splittable) should mark these differing premises, and only them, to be included into the shape."https://gitlab.inria.fr/why3/why3/-/issues/315Too much ghostification?2022-03-22T16:55:27+01:00Benedikt BeckerToo much ghostification?In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from li...In the following example, the ghostification that is introduced by line 16, is expanded to line 12, which results in a compilation error.
The example code works fine when `f` is non-recursive, when the `ghost` keyword is removed from line 16, or when an `; ()` is added after line 16.
```
$ cat test.mlw
module Test
use option.Option
let ref x = ()
exception E
type t = A | B
let rec f (t: t) diverges raises { E -> true } =
match t with
| A ->
x <- () (* Line 12 *)
| B ->
try
f t;
ghost () (* Line 16 *)
with E ->
raise E
end
end
end
$ why3 extract --modular -D ocaml64 -L . test.Test -o /tmp
File "./test.mlw", line 12, characters 6-13:
This expression makes a ghost modification in the non-ghost variable x
```Andrei PaskevichAndrei Paskevichhttps://gitlab.inria.fr/why3/why3/-/issues/246Allow "use ghost Foo"2019-05-21T15:37:41+02:00Guillaume MelquiondAllow "use ghost Foo"It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted prog...It might happen that one wants to use a module for specification and ghost code, but not for actual code (and a fortiori extraction). A good example is `int.Int` which is ubiquitous in WhyML programs but not necessarily in extracted programs.
It would be good to have a way in the surface language to express and enforce that such a module is not meant to be actually used. Proposed syntax: `use ghost int.Int`. This would also make the extraction a lot less adhoc with respect to these modules.
A possible implementation would be to flag the corresponding scopes as being restricted. Any symbol accessed through such a scope would be forbidden to occur in non-ghost code. The change in `Why3extract.use_fold` would be trivial.
Open questions:
- what if the user do both `use` and `use ghost`?
- what if the user do `use ghost` on a module with toplevel side effects?https://gitlab.inria.fr/why3/why3/-/issues/51Instantiation of mutable type symbol when cloning2019-01-28T14:35:28+01:00CLOCHARD MartinInstantiation of mutable type symbol when cloningThere are several problems in cloning when dealing with mutable type symbols.
1) One cannot instantiate a private mutable type with a type application:
```
module A0
type t = private mutable {}
end
module A1
use import ref.Ref
cl...There are several problems in cloning when dealing with mutable type symbols.
1) One cannot instantiate a private mutable type with a type application:
```
module A0
type t = private mutable {}
end
module A1
use import ref.Ref
clone A0 with type t = ref int
end
```
fail with error `Illegal instantiation for symbol t`. However, replacing `ref int`
by an alias works. This problem only arises for abstract mutable types.
2) If one instantiate a private mutable type `t` with a non-mutable type in a module
which also contains a `val` taking an element of `t` as argument:
```
module A0
type t = private mutable {}
val g (x:t) : unit
end
module A1
use import list.List
type u = list int
clone A0 with type t = u
end
```
why3 crash with exception `Invalid_argument("Ity.create_region")`.
3) If one attempt to instantiate a non-mutable type with a mutable one, why3 silently
accept the substitution by transforming the mutable type into its snapshot. This lead to
unexpected type errors in other places:
```
module A0
type t
val g (x:t) : unit
end
module A1
use import ref.Ref
type u = ref int
let g (x:u) : unit = x := 0
clone A0 with type t = u, val g = g
end
```
result in an error when instantiating `A0.g` by `A1.g`:
`This application expects a mutable type but receives {ref int}`.https://gitlab.inria.fr/why3/why3/-/issues/27Sequence literals2020-12-17T10:27:16+01:00Guillaume MelquiondSequence literalsCurrently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data struct...Currently, the only non-singleton data structure for which literal constants can be provided is the `list` type. This is especially limiting, since both interpretation and extraction can easily take advantage of random access data structures. So it would be worth having an input syntax for expressing literals for such structures and propagating these constants as far as possible in the system. A few questions to answer:
1. What is the syntax? The OCaml syntax `[| ... ; ... |]` might be fine.
2. What is the type of such a literal? Should it have a fixed type (e.g. `seq 'a`)? Or should its type depend on the context so that one can use this syntax to input program arrays?
3. How should it be translated to provers that do not support such literals? Using `epsilon s. length s = ... /\ s[0] = ... /\ ...` might be both effective and cheap implementation-wise.