CATA: mutual recursion + multi-function relational specs (Contata MR/SO categories)

[alcides]

Context

PR #394 added the feasible subset of the CATA paper's benchmark suite (Miltner, Wang, Chaudhuri & Dillig, Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata; tool Contata). The paper evaluates on 30 benchmarks across four categories:

Category	Count	Example
Mutual recursion (MR)	7	even/odd (evens/odds)
Recursive comparators (RC)	7	int-tuple list equality
Partial data structures (PDS)	12	binary-tree removal
Stack Overflow (SO)	4	reverse a list twice

Only the relational-comparator (RC) flavour is implemented so far (examples/synthesis/cata/{pred,neg,double,square}.ae + succ/pick), since aeon's cata backend synthesizes a single function from a single-function refinement spec.

Problem

The defining features of the paper's suite are out of scope for the current backend:

1. Mutual recursion (the entire MR category) — co-synthesizing two functions (e.g. evens and odds) against a spec that relates them. aeon synthesizes one hole at a time.
2. Relational / k-safety specs relating multiple functions, or multiple runs of one function (much of RC, all of SO, e.g. "reverse a list twice" = f(f(x)) = x). These can't be stated as a single function's refinement.

Proposed direction

Extend the CATA backend toward the paper's actual contribution:

• support multiple simultaneous holes / co-synthesis of mutually-recursive functions;
• accept relational specifications over several functions (k-safety), not just a single function's refinement type;
• realise the constraint-annotation acceptance (over-approximating an unknown callee's I/O behaviour and refining via unsat cores), which aeon currently approximates with the liquid typechecker for a single function.

This is research-grade and is the path to the MR/SO benchmark categories.

References

• Backend: aeon/synthesis/modules/cata/synthesizer.py
• Scope notes: examples/synthesis/cata/README.md
• Paper: Miltner, Wang, Chaudhuri & Dillig, Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automata (tool Contata)