Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Refuting a pathological but reachable pattern with chess #7822

Closed
vicuna opened this issue Jul 16, 2018 · 9 comments

Comments

Projects
None yet
3 participants
@vicuna
Copy link

commented Jul 16, 2018

Original bug ID: 7822
Reporter: @Octachron
Assigned to: @garrigue
Status: confirmed (set by @garrigue on 2018-07-31T10:19:59Z)
Resolution: open
Priority: low
Severity: minor
Version: 4.07.0
Target version: 4.08.0+dev/beta1/beta2
Category: typing
Monitored by: @gasche @yakobowski

Bug description

When typing overly complex refutation clauses, it is possible to exploit the lack of backtracking for ident binding time in the counter-example search to go beyond the authorized number of existential variables during the search and then refute the pattern even if counter-examples exist further down in the search tree.

As an illustration, the attached file construct a type level encoding of
of a piece moving on a 4×4 board and then proceed to simultaneously
refute the existence of hamiltonian paths and produce a hamiltonian path
as a counter-example (by pruning the search path and avoiding the issue above).

Does this count as a bug?

File attachments

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 16, 2018

Comment author: @gasche

Clearly the most beautiful bug this month -- for now.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 30, 2018

Comment author: @garrigue

Using ocaml 4.06.1, the search seems to go on forever.
What version did you use?

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 30, 2018

Comment author: @Octachron

I tested on 4.07.0, where it only takes few seconds to fail on the second refutation clause.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 31, 2018

Comment author: @garrigue

For the second clause, it indeed produces a counter example.
My question was for the first clause. How long does it take to be accepted without warning?
For me on MacOS, it just goes on forever, so the bug does not appear.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 31, 2018

Comment author: @garrigue

Sorry. Indeed on 4.07.0, and on the 4.07 branch the first clause succeeds pretty fast too.
However on 4.06.0 it goes on forever, whereas the allowed number of existentials is supposed to be lower.
Mystery in the search.

@vicuna

This comment has been minimized.

Copy link
Author

commented Jul 31, 2018

Comment author: @Octachron

On 4.06.1, it takes me ~ 10 minutes to find a counter-example for the first refutable clause. I have another example with a 3×4 board where it only takes ~ 30 seconds to find a counter-example with 4.06.1 (whereas 4.07 still fail to find it). Should I upload it?

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 1, 2018

Comment author: @garrigue

For there record:

there_are_no_wazir_tours (Right::Right::Up::Up::Left::Down::Left::Up::Left::Down::Down::Down:: Right::Right::Right::[]);;
Exception: Match_failure ("//toplevel//", 1, 59).

Turning it into a segfault should be easy (using the result type).

@vicuna

This comment has been minimized.

Copy link
Author

commented Aug 1, 2018

Comment author: @garrigue

There is now a GPR fixing that.
Please review :)

#1951

@vicuna vicuna added the typing label Mar 14, 2019

@vicuna vicuna added this to the 4.08.0 milestone Mar 14, 2019

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Mar 15, 2019

Fixed by #1997.
Unfortunately, the search takes so long that we cannot add this to the test suite.

@garrigue garrigue closed this Mar 15, 2019

@vicuna vicuna added the bug label Mar 20, 2019

@nojb nojb modified the milestones: 4.08.0, 4.08 Mar 29, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.