tests: make the query and search tests assert results

[dingf3ng]

Why

Both test files reported success while checking nothing.

test_context_search.py scored successful_searches > 0, where a "success" was any string coming back from coq.search(). It built its interface as CoqInterface(path) — no workspace, no library_paths — so libframac was never mapped, the goal file's statement didn't typecheck, no proof opened, and load() died in coqpyt with IndexError: pop from empty list.

The return value of load() was discarded and "✅ CoqInterface loaded successfully" printed regardless. All 15 queries then returned the string "aux_file not accessible" and each was counted as a hit:

📊 Successful queries: 15/15
📊 Successful tests: 12/12
exit 0, in 12 seconds

Under pytest it was worse — both functions return a bool, which pytest discards:

PytestReturnNotNoneWarning: Test functions should return None, but ... returned <class 'bool'>
2 passed, 2 warnings in 14.58s

Green unconditionally. test_coq_interface_queries.py had the same construction and the same scoring, reporting 23/23.

What changed

Both now build the interface from configs/default_config.json and assert load().

Queries are checked by content, never by size:

query	must contain
Search Z.abs	Z.abs_0
Locate mult	Corelib.Init.Peano.mult
Check (fun x => x + 1)	fun x : int => x + 1

Sizes and exact text drift with the Rocq version and with which notations are in scope, so only substrings are asserted. The three searches too large to pin that way assert a size floor instead.

One assertion is load-bearing: Search Z.abs must contain Abs.Abs_pos, which lives in libautorocq/int/Abs.v. It fails if the libframac mapping isn't actually on the load path — the exact defect that made the file vacuous.

Reduction and ranking are tested directly, not through Rocq

Which size band a live query lands in is decided purely by len(content), and real output sits right on the boundaries — Search to_sint32 is 503 characters against a 500-char threshold. Three characters of library drift would silently delete that coverage with nothing failing.

So ResultReducer is driven directly with synthetic input, pinning all four bands, both sides of 500/501 and 1000/1001, and the goal-context ranking. Instant, no coq-lsp.

Verified by mutation

mutation	result
remove workspace	3 tests fail — pop from empty list
wrong expected fragment	fails, printing the real output
wrong expected reduction band	fails, naming both