MantisBT - OCaml
View Issue Details
0007822OCamltypingpublic2018-07-16 13:592018-08-01 07:32
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.
? (3,811) 2018-07-16 13:59
Issue History
2018-07-16 13:59octachronNew Issue
2018-07-16 13:59octachronFile Added:
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

2018-07-16 14:02   
Clearly the most beautiful bug this month -- for now.
2018-07-30 09:52   
Using ocaml 4.06.1, the search seems to go on forever.
What version did you use?
2018-07-30 10:04   
I tested on 4.07.0, where it only takes few seconds to fail on the second refutation clause.
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.
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.
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?

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).
2018-08-01 07:32   
There is now a GPR fixing that.
Please review :) [^]