Build the Oddly Exact proof theater and strengthen numeric provenance - #29
Draft
copyleftdev wants to merge 10 commits into
Draft
Build the Oddly Exact proof theater and strengthen numeric provenance#29copyleftdev wants to merge 10 commits into
copyleftdev wants to merge 10 commits into
Conversation
|
Important Review skippedDraft detected. Please check the settings in the CodeRabbit UI or the ⚙️ Run configurationConfiguration used: defaults Review profile: CHILL Plan: Pro Plus Run ID: You can disable this status message by setting the Use the checkbox below for a quick retry:
✨ Finishing Touches🧪 Generate unit tests (beta)
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
A solve costs 0.26ms. Spawning the CLI to perform it costs 1.36ms. The process was five times the work, which is the entire argument for a server — not that the arithmetic is slow, but that fork+exec around it is. So the endpoint that matters is /v1/batch. A caller with 212 solves to do — one stress test — asks once, and the calls fan out across cores. Measured here: 212 linear solves in 1.3ms of compute, against 84ms for the same work in WebAssembly and 344ms through 212 CLI spawns. Every request goes through execute_tool_json, the same function the CLI and the wasm build call. Not a port of it — the same code, three transports. Feature gated, so none of it reaches the default build or the wasm target. AND A CONFORMANCE HARNESS, WHICH FOUND SOMETHING ON ITS FIRST RUN 3 of 36 cases diverge between the CLI binary and the calcd binary, in the last bit or two of an f64. WASM matched the CLI on all 36; only the two native binaries disagree. Ruled out by measurement, in order: input encoding (byte-identical strings reach the kernel, verified by echoing both); Cargo feature unification (no maths crate changes features under --features server); the FPU control word (MXCSR 0x1f80 on main and worker threads alike — no FTZ, no DAZ, round-to-nearest); and thread identity (it reproduces on a single thread). What is left is codegen — the same source in two binaries with different dependency graphs. The size of the number is not the point. Everything bento displays is rounded to dollars. The exposure is the seal: a signature over a hash of the figures, and a hash has no bit that matters less than the others. The same model solved on the server and verified against a browser solve would hash differently and read as tampering. A sealed artifact must therefore be computed by one transport end to end, and this harness has to gate deployment rather than run occasionally. The corpus is every request shape bento actually issues across its four worlds, because the shapes a real caller sends are the ones worth guaranteeing.
The first version blocked on any difference at all, which made it useless: 3 of 36 cases differ between the CLI and calcd binaries in the fifteenth significant figure, nobody can fix that today, and a permanently red check is one everybody learns to ignore. So it now separates what a caller can act on from what they cannot. MUST covers anything that changes a decision or a displayed figure — feasibility, a survivor count, a dollar — and blocks. NOTE covers last-bit float drift below 1e-9 relative and is recorded. Measured in the product rather than assumed: routing a 121-cell survival map through calcd instead of the browser moved 13 cells in the fifteenth figure and changed no feasibility, no survivor count and no edge. And a correction to the previous commit message, which claimed this drift would make a sealed pack read as tampering. It does not. Verification re-hashes the claims carried inside the pack; it never re-solves the model, so the figures travel with the signature and there is nothing to disagree with at verification time. Checking that beat assuming it.
Two-stage: dependencies compile against the manifests alone so a change to src does not rebuild nalgebra, then the real sources. Runtime is debian-slim with the binary and nothing else, 136MB, running unprivileged. It binds 0.0.0.0 because it is meant to be an internal service behind something that checks entitlement — it solves whatever it is handed and asks nobody for permission, which is exactly why it must not be routable from outside. Verified in a clean container: 212 solves in 5.7ms, objective identical to the host build.
A linear program with no solution was reported as status "error" with code
"invalid_input". That says the request was malformed. The request was perfectly
good — it was the plan that could not be made to work, which is the one fact the
caller needed and the only one the response did not contain.
Found by dogfooding: a construction startup's model went infeasible the moment
its 75-day payment terms were included, and the kernel's answer was that the
question had been asked wrongly.
So three outcomes are now three statuses, the way every real solver reports them:
infeasible the constraints admit no point. An answer.
unbounded the objective improves without limit. Also an answer, and almost
always a missing constraint rather than a bad request.
error the request itself is wrong. Still invalid_input, still rejected.
Both solve paths were conflating them. The MILP returned Err for infeasibility,
and the continuous path flattened good_lp's ResolutionError — which already
separates Unbounded and Infeasible from everything else — into one string.
Branch and bound also pruned on any error at all, so a solver that misbehaved
mid-search would have been reported as a plan that cannot work: a wrong answer
wearing a right one's face. It now prunes the two that mean "nothing down here"
and surfaces the one that means the solver broke.
The existing test asserted the old behaviour, so its failure is what proved the
change landed; it now asserts the distinction instead. Four conformance cases
pin the statuses across all three transports, including the malformed request,
because a distinction only means something if both sides of it hold.
No published schema or contract text enumerated response statuses, so nothing
advertised is contradicted by adding two.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What changed
Why
The article’s central claim is that a green test is evidence only when its oracle is independent and its assertions are capable of exposing the defect. This change makes that claim executable: the new regression test derives standard errors from a closed-form oracle, checks the complete vector, and deliberately includes a point where one component collides under the plausible
r*q -> r+qmutant.The pricing additions apply the same discipline to financial models by keeping decimal inputs and DCF calculations exact as rationals, then checking them against an independent 256-bit implementation.
Validation
The pre-commit gate passed:
cargo fmtcargo checkcargo clippycargo testsuite (405 unit tests plus all integration suites)cargo packageMutation replay was also performed locally: the exact standard-error
* -> +mutant and the alternate(v/s) -> (v*s)mutant both turn the new closed-form test red, while the correct implementation remains green.