Translation-validator ergonomics for a consumer migrating a per-run validator (loom)
Three small, non-fragment API asks that make migrating a per-run translation validator onto ordeal mechanical. None is a blocker (companion to the symbolic-array fragment extension, which is the real gate); all are API/ergonomics.
(a) Wall-clock deadline on check. A consumer's validator degrades a slow solve to a fast, safe revert to avoid CI hangs (it drives a per-check millisecond budget, X ms default, 0 = off, → Unknown on exhaustion). ordeal offers check_with_limit(max_conflicts) — a conflict budget, not a time budget. Ask: either a check_with_deadline(Duration) wrapper, or a documented conflict-budget↔latency calibration so a consumer can map a ms budget onto conflicts.
(b) prove_equiv over the sliver. Solver::prove_equiv(a, b) exists for pure BvTerm. Ask a sliver analogue — a one-call "prove two encoded results equivalent, with memory/UF context" over ExtBvTerm (a check_sliver-based equivalence entry), so consumers don't hand-assemble the Ne goal + congruence context. Keeps the pure and memory/UF paths symmetric.
(c) Public "is this term a ground constant → value" helper. ordeal has eval::eval_bv internally; expose a small eval-backed query so a consumer can fold a concrete-operand result term-side (a validator has a fast path that reads a concrete value off a term). Lowest priority — the consumer can keep this fold on its own side.
Type: API/ergonomics. Refs: the loom→ordeal migration gap analysis.
Translation-validator ergonomics for a consumer migrating a per-run validator (loom)
Three small, non-fragment API asks that make migrating a per-run translation validator onto ordeal mechanical. None is a blocker (companion to the symbolic-array fragment extension, which is the real gate); all are API/ergonomics.
(a) Wall-clock deadline on
check. A consumer's validator degrades a slow solve to a fast, safe revert to avoid CI hangs (it drives a per-check millisecond budget,Xms default,0= off, →Unknownon exhaustion). ordeal offerscheck_with_limit(max_conflicts)— a conflict budget, not a time budget. Ask: either acheck_with_deadline(Duration)wrapper, or a documented conflict-budget↔latency calibration so a consumer can map a ms budget onto conflicts.(b)
prove_equivover the sliver.Solver::prove_equiv(a, b)exists for pureBvTerm. Ask a sliver analogue — a one-call "prove two encoded results equivalent, with memory/UF context" overExtBvTerm(acheck_sliver-based equivalence entry), so consumers don't hand-assemble theNegoal + congruence context. Keeps the pure and memory/UF paths symmetric.(c) Public "is this term a ground constant → value" helper. ordeal has
eval::eval_bvinternally; expose a smalleval-backed query so a consumer can fold a concrete-operand result term-side (a validator has a fast path that reads a concrete value off a term). Lowest priority — the consumer can keep this fold on its own side.Type: API/ergonomics. Refs: the loom→ordeal migration gap analysis.