Exact

Exact Union RegExp

Repository files (latest commit first)

Filename	Latest commit message	Latest commit date
Transaction Science fa88c5c9d2 Merge origin/main into ar-1-on-main — reconcile the two stand-in markers ... Main landed PR #62's soundness work (`Solver::is_reference_stub`, `CascadeResult::closed_by_stub`, `require_substantive_proof`, and proof-conformance's `soundness.rs`) after this branch diverged. That work and the ladder fix here address the same defect from opposite ends: * main **detects** a fabricated proof — the stand-ins declare themselves, the result is marked, the cache does not launder the marker, and a relying party can refuse it. * this branch **prevents** it — the real ladders hold decision procedures only, so a solverless machine yields Unproved instead of escalating into a rung that proves anything. Both are wanted, but two overlapping markers are worse than one. Resolution: * Dropped `is_decision_procedure` in favour of main's published `is_reference_stub`, and re-expressed `ladder_is_sound` in its terms. The marker I added had the safer default (a new stand-in is excluded unless it claims to be checkable) but a second trait method meaning nearly the same thing is a worse outcome than losing that default. * Recovered the safety that default was buying at the ladder instead: `ladder_is_sound` now also pins the real ladders' exact tiers, so a stand-in that forgets to override `is_reference_stub` still cannot slip in unnoticed. Documented on the trait so the two halves are findable together. * `soundness.rs`'s `a_stand_in_proof_is_detectable_before_it_is_trusted` proved an open conjecture through `real_ladder()` to demonstrate detection. That premise is gone — it now exercises `reference_ladder()`, where stand-ins legitimately live, and the property it tests is unchanged. * Added `the_real_ladder_never_reaches_a_stand_in` as its companion. Detection is a last line of defence that only works if the relying party remembers to call it; not reaching a stand-in at all does not depend on anyone remembering. Note the defect was still live on main: main's `real_ladder()` still ends in `FrontierModel`, and main's own `joulecontract-proof` test asserts the SMT rung returns Unproved when no solver is present — which fails there on any machine without `z3`. 402 tests pass across proof-rs, joule-code and joulecontract, both with and without `z3` on PATH. The conformance vector pack is byte-identical. Co-Authored-By: Claude Opus 5 <[email protected]>		2026-08-29 05:13:10 -04:00
..
lib.rs	Merge origin/main into ar-1-on-main — reconcile the two stand-in markers	2026-08-29 05:13:10 -04:00
prop.rs	Add the proof open standard — a carrier for verified work	2026-06-07 15:30:07 -04:00