nl-frontier: pick up the per-argument hosts cvc5 now reports, and check why at stays null

[kiranandcode]

BasisResearch/cvc5#9 (at 312ca61) changes the (get-info :nl-frontier) reply in two ways that concern -V nl-frontier. Neither breaks anything today; one of them improves Verus output for free, and one needs a change here to be used.

What changed in the reply

1. Every (:term ...) inside :args now ends with a :hosts (...) list, of exactly the shape an atom's :hosts already has. An argument can be where a term entered the problem even when the atom around it is one the rewriter built.
2. An integer division is now also hosted by a modulus over the same operands. Operator elimination rewrites (mod n d) as n - d * (div n d), so what reaches arithmetic is a division, and the reply used to look only for a division host. Verus writes a % d as EucMod, so every such atom had no host at all.

Compatibility: nothing to do

parse_nl_term in source/air/src/smt_verify.rs walks items.chunks(2) and ignores key/value pairs it does not recognise (_ => {}), so the new :hosts inside a :term parses harmlessly. Confirmed by running the current main build (a685f844) against the new cvc5: the reply parses, every atom comes through, no error.

What Verus gains without any change

Same verus binary, only VERUS_CVC5_PATH swapped, on tests/fixtures/nl_frontier_division.rs from verus-tools-mcp:

cvc5	the two division atoms
before	hosts: []
after	hosts of 3, naming ((a + (k * d)) % d), the modulus the source wrote

The product atoms are unchanged (0 and 4 hosts). So bumping the pin alone turns the division atoms from unlocated into located.

What needs a change here

parse_nl_term drops the new :hosts, so ResolvedNlTerm carries none and best_location never sees them. The case this loses is an atom the rewriter built around an argument the source did write. Dividing by a sum, a / (b + 1), distributes (* (+ 1 b) q) into (+ q (* b q)), so the atom is b * (a / (b + 1)), a product no source term applies: its own host list is honestly empty, while its argument names the EucDiv. Picking the argument hosts up means adding a hosts field to ResolvedNlTerm and letting best_location fall back to them when the atom has none.

Separate observation about at

In the run above, at and at_basis come back null for every atom in that fixture, including the product that has four hosts, and both before and after the cvc5 change. So this is not about missing hosts. best_location in rust_verify/src/provenance.rs chooses the span, and its "query" | "goal" branch does not appear to fire even though the input host carries a query tag. Worth a look independently of the above.

Repro

# a cvc5 built from BasisResearch/cvc5 at 312ca61
VERUS_CVC5_PATH=<that binary> VERUS_MCP_ENABLED=1 \
  verus --crate-type=lib -V nl-frontier --output-json \
  <verus-tools-mcp>/tests/fixtures/nl_frontier_division.rs

Prerequisite for any of this landing: tools/common/solvers.toml still pins fork main at b25a419c78, so the pin needs a bump past cvc5#9 first.

[kiranandcode]

Re-checked against main at 1a780498c, after #20 merged and the pin moved. Two corrections to the issue above.

The pin is no longer b25a419c78. tools/common/solvers.toml now reads tag = "basis-c893833109", fork main at c893833, the same main cvc5#9 sits on top of. So the prerequisite is a bump past cvc5#9 from there.

The parser is still compatible. #20 rewrote a good deal of provenance.rs, air/src/context.rs and air/src/smt_verify.rs, but it left parse_nl_term, parse_nl_atom and best_location alone. Rebuilt main at 1a780498c and ran it against a cvc5 built from BasisResearch/cvc5#9 at 5ede340: the reply parses, four atoms come through, and both division atoms carry three hosts naming ((a + (k * d)) % d). The pinned cvc5 produces no nl_frontier block at all, since the cvc5 side of this is still the open PR.

Everything else in the issue stands: parse_nl_term drops the new per-argument :hosts, and at comes back null for every atom in that fixture including the product with four hosts.