MantisBT - OCaml
View Issue Details
0007822OCamltypingpublic2018-07-16 13:592018-08-01 07:32
octachron 
garrigue 
lowminoralways
confirmedopen 
4.07.0 
4.08.0+dev 
0007822: Refuting a pathological but reachable pattern with chess
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?
No tags attached.
? minichess.ml (3,811) 2018-07-16 13:59
https://caml.inria.fr/mantis/file_download.php?file_id=1748&type=bug
Issue History
2018-07-16 13:59octachronNew Issue
2018-07-16 13:59octachronFile Added: minichess.ml
2018-07-16 14:02gascheNote Added: 0019249
2018-07-30 09:17garrigueAssigned To => garrigue
2018-07-30 09:17garrigueStatusnew => assigned
2018-07-30 09:52garrigueNote Added: 0019281
2018-07-30 09:52garrigueStatusassigned => feedback
2018-07-30 10:04octachronNote Added: 0019282
2018-07-30 10:04octachronStatusfeedback => assigned
2018-07-31 12:13garrigueNote Added: 0019285
2018-07-31 12:13garrigueStatusassigned => feedback
2018-07-31 12:19garrigueNote Added: 0019286
2018-07-31 12:19garrigueStatusfeedback => confirmed
2018-07-31 12:21garrigueProduct Version => 4.07.0
2018-07-31 12:21garrigueTarget Version => 4.08.0+dev
2018-07-31 12:27octachronNote Added: 0019287
2018-07-31 12:27octachronNote Edited: 0019287bug_revision_view_page.php?bugnote_id=19287#r3309
2018-08-01 07:32garrigueNote Added: 0019289
2018-08-01 07:32garrigueNote Added: 0019290

Notes
(0019249)
gasche   
2018-07-16 14:02   
Clearly the most beautiful bug this month -- for now.
(0019281)
garrigue   
2018-07-30 09:52   
Using ocaml 4.06.1, the search seems to go on forever.
What version did you use?
(0019282)
octachron   
2018-07-30 10:04   
I tested on 4.07.0, where it only takes few seconds to fail on the second refutation clause.
(0019285)
garrigue   
2018-07-31 12:13   
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.
(0019286)
garrigue   
2018-07-31 12:19   
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.
(0019287)
octachron   
2018-07-31 12:27   
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?

(0019289)
garrigue   
2018-08-01 07:32   
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).
(0019290)
garrigue   
2018-08-01 07:32   
There is now a GPR fixing that.
Please review :)

https://github.com/ocaml/ocaml/pull/1951 [^]