why3 issueshttps://gitlab.inria.fr/why3/why3/-/issues2024-03-28T09:36:21+01:00https://gitlab.inria.fr/why3/why3/-/issues/842why3 execute type inference problem2024-03-28T09:36:21+01:00Delphine Demangewhy3 execute type inference problemI came across a surprising behavior of the `why3 execute` command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
```
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue ...I came across a surprising behavior of the `why3 execute` command (why3 plateform 1.6.0).
Here's a shrinked example, to help reproducing the error.
```
module Issue
use bintree.Tree
use bintree.Inorder
use list.List
let issue () =
let l = inorder Empty in
assert { l = Nil }
end
```
With `why3 ide`, it behaves as excepted : one VC is generated, and the assertion is easily discharged automatically.
With `why3 execute`, I get the following error message :
```
$ why3 execute issue.mlw --use=Issue 'issue ()'
Type mismatch between bintree.Tree.tree 'a and bintree.Tree.tree 'xi
```
Is this a known issue for version 1.6.0 of why3 ?
I have tried to provide more guidance to type inference using type annotations, but this doesn't solve the problem.
Thanks1.7.2MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/841using `model_projection` on alias types should be forbidden2024-03-26T11:09:02+01:00MARCHE Claudeusing `model_projection` on alias types should be forbiddenthe meta `model_projection` has the following form
```
meta "model_projection" function f
```
where `f` is a unary function say from some type `t`. It allows to obtain values in counterexamples say when `t` is an abstract type. It can al...the meta `model_projection` has the following form
```
meta "model_projection" function f
```
where `f` is a unary function say from some type `t`. It allows to obtain values in counterexamples say when `t` is an abstract type. It can also be used when `t` is not abstract. Yet, when `t` is an alias type then the current implementation produces some unexpected behavior, and indeed it is unclear what should be done in such a case. It is thus preferable that Why3 simply signals an error when `t` is an alias type.1.7.2MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/840spurious debug messages when using `why3 session create`2024-03-26T11:03:17+01:00MARCHE Claudespurious debug messages when using `why3 session create`executing `why3 session create` displays spurious debug messages regarding the directory and the session file created. They should be visible only when some debug flag is setexecuting `why3 session create` displays spurious debug messages regarding the directory and the session file created. They should be visible only when some debug flag is set1.7.2Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/839forward_propagation strategy : sin and cos support2024-03-05T12:17:02+01:00BONNOT Paulforward_propagation strategy : sin and cos supportBONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/838Problem with instantiation of interfaces2024-03-19T14:29:57+01:00Mário PereiraProblem with instantiation of interfacesConsider the following piece of WhyML code:
```
module M
type t 'a = 'a -> int
end
module N : M
end
```
Let us assume this is the contents of a `foo.mlw` file. If we use `why3 prove foo.mlw`, then Why3 replies with the error
```...Consider the following piece of WhyML code:
```
module M
type t 'a = 'a -> int
end
module N : M
end
```
Let us assume this is the contents of a `foo.mlw` file. If we use `why3 prove foo.mlw`, then Why3 replies with the error
```
Symbol t not found in implementation
```
However, if we change module N into
```
module N : M
type t 'a = 'a -> int
end
```
then we get the error
```
Cannot instantiate a defined symbol t
```Benjamin Terra-JorgeBenjamin Terra-Jorgehttps://gitlab.inria.fr/why3/why3/-/issues/836Use clone for ufloat theory2024-02-23T11:20:11+01:00BONNOT PaulUse clone for ufloat theoryProvide a generic theory parametrized by `eps` and `eta`, and clone it for single and double precision.
Also separate ufloat theorems in an other module.Provide a generic theory parametrized by `eps` and `eta`, and clone it for single and double precision.
Also separate ufloat theorems in an other module.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/834Case insensitive filter prover2024-02-12T15:45:51+01:00François BobotCase insensitive filter proverRemove the generation of shortcut from the section header of prover-data-conf and make the filtering of prover case insensitive.
TODO: check that for all prover it will not change the shortcut or add an explicit one
FYI @x-ABlancRemove the generation of shortcut from the section header of prover-data-conf and make the filtering of prover case insensitive.
TODO: check that for all prover it will not change the shortcut or add an explicit one
FYI @x-ABlancFrançois BobotFrançois Bobothttps://gitlab.inria.fr/why3/why3/-/issues/829Fix the generation of proof taks by the RAC2024-01-16T13:55:34+01:00MARCHE ClaudeFix the generation of proof taks by the RACThe RAC generates proof tasks for checking assertion. This task generation is implemented by some ad-hoc
cloning of the module from which the executed function comes from. This cloning is incorrect in general, as shown by various error m...The RAC generates proof tasks for checking assertion. This task generation is implemented by some ad-hoc
cloning of the module from which the executed function comes from. This cloning is incorrect in general, as shown by various error messages that appear in the check-ce bench after the MR !992 is merged.1.8.0MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/823Unexpected inconsistency with (<>)2024-01-04T09:26:46+01:00Xavier DenisUnexpected inconsistency with (<>)I stumbled across the following unexpected inconsistency in why3's handling of `<>`.
The following program compiles:
```
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
However, this one does ...I stumbled across the following unexpected inconsistency in why3's handling of `<>`.
The following program compiles:
```
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
However, this one does not:
```
use int.Int
type option 'a = Some 'a | None
let rec ghost function f (x y : option int) = x <> y
```
Stating,
```
File "test.mlw", line 5, characters 46-47:
This expression has type Top.option int, but is expected to have type int
```
I believe this is due to how `<>` is treated _literally_ as `not (a = b)` and since `int.Int` furnishes a `=` symbol this is used in the expansion, however its strange that if that module is _not_ imported then we get the polymorphic mathematical equality instead.https://gitlab.inria.fr/why3/why3/-/issues/822Allow extracting floating-point literals2023-12-21T11:43:32+01:00Guillaume MelquiondAllow extracting floating-point literalsThe extraction code (both in the common part `compile.ml` and in the specific parts `ocaml.ml` and `c.ml`) chokes on real literals.
```whyml
use ieee_float.Float64
let const = (2.0 : Float64.t)
(* why3 extract -D ocaml64 foo.mlw *)
```The extraction code (both in the common part `compile.ml` and in the specific parts `ocaml.ml` and `c.ml`) chokes on real literals.
```whyml
use ieee_float.Float64
let const = (2.0 : Float64.t)
(* why3 extract -D ocaml64 foo.mlw *)
```1.8.0https://gitlab.inria.fr/why3/why3/-/issues/821Add a way to debug Z3 proofs in the IDE2023-12-13T13:38:33+01:00BONNOT PaulAdd a way to debug Z3 proofs in the IDEZ3 can produce a trace of its execution.
It would be useful to be able to get some useful data from it in the IDE.
The most interesting thing to extract would certainly be the quantifiers instantiations that have been performed.Z3 can produce a trace of its execution.
It would be useful to be able to get some useful data from it in the IDE.
The most interesting thing to extract would certainly be the quantifiers instantiations that have been performed.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/818stop displaying counterexamples sorted by lines in the source2023-11-28T14:40:39+01:00MARCHE Claudestop displaying counterexamples sorted by lines in the sourceThe counterexamples are currently displayed by why3 in a manner that is somehow "sorted" by lines in the source.
This display is anyway, generally, too much detailed by default.
The default way to display a counterexample should be to o...The counterexamples are currently displayed by why3 in a manner that is somehow "sorted" by lines in the source.
This display is anyway, generally, too much detailed by default.
The default way to display a counterexample should be to only display the values given as input to the function under proof. These values are exactly the ones that are collected as initial values for running the small-step RAC.
As options, and only when these options are set by the user, Why3 could display:
- the values of the variables at the location of the VC
- the values of the variables at the position of function calls and loops (the one that are collected for the giant-step RAC)
- the full set of values, as it is for now. But the values coming from other modules (in particular the standard library) could be filtered outMatteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/817feature wish: debug flag to print the location of checked formulas in the RAC2023-11-28T14:06:16+01:00MARCHE Claudefeature wish: debug flag to print the location of checked formulas in the RACTo better debug the checking of counterexamples, it would be better to have a debug flag that will trace on which formulas of the source the RAC prover is called. There is an example coming from spark where the prover is called several h...To better debug the checking of counterexamples, it would be better to have a debug flag that will trace on which formulas of the source the RAC prover is called. There is an example coming from spark where the prover is called several hundred of times, which is unexpected.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/815Identify users missing a `gitlab.com` account2023-11-13T14:30:53+01:00Xavier DenisIdentify users missing a `gitlab.com` accountTo prepare for a migration to `gitlab.com` we should identify contributors who do not have a matching account.To prepare for a migration to `gitlab.com` we should identify contributors who do not have a matching account.https://gitlab.inria.fr/why3/why3/-/issues/814Highlighting in the IDE is broken for counterexamples2023-11-08T11:34:24+01:00BONNOT PaulHighlighting in the IDE is broken for counterexamplesThe color highlighting is broken for counterexamples panel, as it seem to highlight random parts of the text.The color highlighting is broken for counterexamples panel, as it seem to highlight random parts of the text.https://gitlab.inria.fr/why3/why3/-/issues/812Extend behaviour of eliminate_epsilon2023-10-30T10:55:00+01:00Matteo ManighettiExtend behaviour of eliminate_epsilonThe eliminate_epsilon transformation in Spark has a broader scope than the current in Why3. This ticket is to investigate merging the two.The eliminate_epsilon transformation in Spark has a broader scope than the current in Why3. This ticket is to investigate merging the two.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/811Map encoding and polymorphism2024-02-13T15:59:21+01:00Johannes KanigMap encoding and polymorphismWe are generating code that uses generic structures such as maps. Ideally we would like to select the appropriate SMT encoding as late as possible, ideally in the prover driver. For example for maps, one can select the SMTlib theory of a...We are generating code that uses generic structures such as maps. Ideally we would like to select the appropriate SMT encoding as late as possible, ideally in the prover driver. For example for maps, one can select the SMTlib theory of arrays, or use an abstract type with get/set functions and axioms.
If we use the Why3 theory map.Map in the generated code, then we have two choices:
1. we can encode it to SMT arrays as is done e.g. in `smtlibv2.gen`; this works well.
2. we can choose to not do that; in this case, we would get extra "noise" due to the encoding of polymorphism.
There is another option to not use map.Map, and instead define an abstract (non-polymorphic) map type with fixed index and component types, get/set functions and the axioms. Given the cloning mechanism of Why3, this is still entirely generic, as one can do something like this:
```
module Gen_Map
type map
type index_type
type component_type
function get (m : map) (i : index_type) : component_type
...
end
...
clone Gen_Map with type index_type = int, component_type = comp
```
This has the advantage of avoiding the polymorphism encoding. However, using this variant, we have given up (1) above, we can't map this type to SMTlib arrays.
This has the effect that we are essentially deciding at code generation time whether to use SMTlib array encoding or not.
Now my question: Is there a way to write why3 code in such a way that one can select (at the driver level) whether to use SMTlib arrays or whether to use an abstract type (without polymorphism encoding)? If this involves writing e.g. a transformation, that would be an option for us.Matteo ManighettiMatteo Manighettihttps://gitlab.inria.fr/why3/why3/-/issues/809Improvements on goal oriented strategies2023-10-23T17:09:47+02:00BONNOT PaulImprovements on goal oriented strategiesExplore a way to have more control on the flow of execution of goal oriented strategies.
One thing that would be interesting would be to choose the next strat to apply based on the result of a strategy, ie. dynamically generate an order ...Explore a way to have more control on the flow of execution of goal oriented strategies.
One thing that would be interesting would be to choose the next strat to apply based on the result of a strategy, ie. dynamically generate an order of execution.
For instance, we could apply a transformation that generates a list of subtasks, and then instead of applying strats to the subtasks in the subtasks creation order, the order is specified by the strategy.BONNOT PaulBONNOT Paulhttps://gitlab.inria.fr/why3/why3/-/issues/807Why3 should allow to compile several engines for invariant inference simultan...2023-10-06T15:34:04+02:00MARCHE ClaudeWhy3 should allow to compile several engines for invariant inference simultaneouslyThe function `Vc.set_infer_invs` allows to record one engine to infer invariants, if one records a second it will replace the former recorded one. We should allow several such engines.The function `Vc.set_infer_invs` allows to record one engine to infer invariants, if one records a second it will replace the former recorded one. We should allow several such engines.MARCHE ClaudeMARCHE Claudehttps://gitlab.inria.fr/why3/why3/-/issues/805Error with function literals2023-09-29T11:50:18+02:00Xavier DenisError with function literalsI was trying to use function literals as a way to encode sequence literals, but very quickly hit an issue:
```
use seq.Seq
let boom x : seq int = Seq.create 1 [| x |]
```
The following program fails to load saying `File "../broken.ml...I was trying to use function literals as a way to encode sequence literals, but very quickly hit an issue:
```
use seq.Seq
let boom x : seq int = Seq.create 1 [| x |]
```
The following program fails to load saying `File "../broken.mlw", line 3, characters 28-29: Logical symbol (=) is used in a non-ghost context`
It seems like the desugaring for function literals does not work well in program contexts?