[avrabe]

This does both asks in #433. Each has its own oracle, and I watched each one go red before the change.

1. Bump ordeal from 0.30.0 to 0.33.0 (soundness fix ordeal#247)

Oracle: a_query_variable_cannot_masquerade_as_a_sliver_read. It drives the issue's exact counterexample, select(memory, 5) != $sel:memory:5, through BoundedOrdealSolver, the production RuleSolver. The query is satisfiable because the two sides are independent.

ordeal	verdict
0.30.0	Proven, with a certificate that rechecks. This is the bug, reproduced through loom's own path.
0.33.0	Disproven

Was loom's production path exposed? No, and I checked. I found 137 naming calls (BV/Bool/Array new_const/fresh_const, FuncDecl::new) in non-test loom-core code:

• 132 are literals or format templates, and every one begins with a letter (param…, global…, pure_call_…, mem_after_call_…, f32_…).
• The other 5 are pass-throughs: decl_name = "pure_call_{func_idx}", and three rule_solver sites that re-lower names the reflector read back from those same Z3 ASTs.

A collision needs a name that starts with $. The sliver's only production input is decide_bv_equivalence, which receives those ASTs.

2. lower_goal_ne uses Solver::from_sliver

From 0.33.0, only a solver built by from_sliver runs ordeal's trusted, Lean-proven check_sliver_lowering before it returns a verdict. The old path called sliver::lower and asserted the core by hand, which skipped that check.

Oracle: memory_obligations_are_decided_on_the_proven_sliver_path. It asserts Solver::is_sliver() for a memory goal, and not for a pure one. I extracted the construction into solver_for_goal_ne without changing behavior first. The test was then red on 0.33.0 with the old path, and it went green after the switch. No direct sliver::lower call remains in non-test code.

The reasons for avoiding the one-shot helpers (#347) still hold: a refusal is still an Err that the seam defers on, and the deadline still governs the check.

Wiring

Both tests run inside slice 3's verification step (the full suite under both, with the count pinned). To prove that by mutation, I reverted only the from_sliver call: the wired step went [FAIL] and named the new test (567 passed; 1 failed). The pin moves from 566 to 568.

Results

• loom-core with verification: 568 passed under default, both and ordeal
• clippy --all-targets -D warnings: clean
• tools/run_verification.py passes slices 3 and 4
• ordeal 0.33.0 in Cargo.lock, which is what CI builds

Kill-criterion

This change is wrong if any memory or UF verdict comes from a solver with is_sliver() == false, or if the $sel impostor is ever Proven.

One thing would still be false if every check here passed: that an is_sliver() solver gates every verdict, on the entry point loom uses (check_with_deadline), on check_sliver_lowering. That is ordeal's guarantee, documented on Solver::from_sliver, and loom can only observe its precondition. If that guarantee breaks, it should be filed against ordeal.

Merge note

#434 also moves the same slice 3 pin, from 566 to 569. Whichever of the two merges second needs the pin set to 571.

Fixes: #433
Refs: #313

🤖 Generated with Claude Code

https://claude.ai/code/session_01RZof1M5HMBSYVZPeoT4MEn

[github-actions]

Rivet verification gate

✅ 30/38 passed

	count
Passed	30
Failed	0
Skipped (no steps)	8

Filter: (and (= type "feature") (matches id "^TEST-"))

Failed artifacts

(none)

_{Updated automatically by tools/post_verification_comment.py. Source of truth: artifacts/verification.yaml.}