Fix proof-flow evidence logical_id collision on degenerate corpora (CVE-2026-4600) - #132
Draft
jorge-garcia-le wants to merge 1 commit into
Draft
Fix proof-flow evidence logical_id collision on degenerate corpora (CVE-2026-4600)#132jorge-garcia-le wants to merge 1 commit into
jorge-garcia-le wants to merge 1 commit into
Conversation
The mechanical obligation resolver builds Evidence whose identity payload
was only {kind, artifact_digest, observations, provenance}. When many
candidates converge on the same handful of facts — e.g. a single minified
JS bundle like jsrsasign (CVE-2026-4600) — two distinct obligations resolve
off the identical sentinel_use fact via the same deterministic rule, so
their evidence hashes to the same logical_id. The append-only ProofGraph
rejects the second add with 'Evidence ... already exists; append a
successor revision instead', and because apply_resolution's add is
unguarded (engine.py:856) the ValueError aborts the entire run.
C targets never tripped this: distinct facts across a multi-file tree yield
distinct observation sets. A degenerate single-file corpus is the trigger.
Fix:
- Widen Evidence.identity_payload to include supports/contradicts. Evidence
for different claims/obligations is genuinely different logical evidence,
so it gets distinct logical_ids. (Claim identity already carries the
candidate subject + obligation scope, so supports/contradicts differ.)
- Make apply_resolution idempotent as a defensive net: skip re-adding an
evidence/claim whose logical_id is already in the graph, so a genuine
duplicate reuses the stored record instead of aborting the run.
Adds two regression tests reproducing the jsrsasign scenario.
jorge-garcia-le
force-pushed
the
fix/proof-hunt-eval-patches
branch
from
August 6, 2026 22:36
bc27621 to
3b1b6c5
Compare
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
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.
Problem
Running the proof flow against CVE-2026-4600 (jsrsasign) aborts with:
Root cause
Every
VersionedRecordderives itslogical_idby hashing an identity payload. ForEvidence(models.py) that payload was only:{ "kind", "artifact_digest", "observations", "provenance" }The mechanical obligation resolver (
resolvers.py::_resolution) builds evidence from the matching facts, with a constant provenance (producer="mechanical-obligation-resolver", no command / context packet) and observations keyed onfact.id. So when two different obligations (from two different candidates) resolve off the same fact via the same deterministic rule, all four identity fields are byte-identical → identicallogical_id.The append-only
ProofGraph._addtreats a repeatlogical_idas "you must be revising" and raises. That raise is swallowed on the falsifier path (engine.py:580) but not on the resolver path —apply_resolutionatengine.py:856is unguarded, so theValueErrorpropagates out ofarun()and kills the whole run.Why it only surfaced now
Prior proof-flow targets were C (jq, etc.): multi-file trees where facts live at distinct ids/locations, so distinct obligations produce distinct evidence. jsrsasign's entire source is effectively one minified line (
jsrsasign-all-min.js), so ~200 candidates converge on the same handful ofsentinel_usefacts — the first corpus degenerate enough for two mechanical resolutions to be literally identical evidence.Confirmed from the run dir (
results/cve-2026-4600/sh-cbad7381/): the colliding evidence's observations all citefact-d09dfc9df70fa9aeatjsrsasign-all-min.js:225, kindstatic_sentinel_definition, constant mechanical provenance. Two obligations (obligationl-f69a6adac865f0c2and a sibling) claim it.Fix
Evidence.identity_payloadto includesupports/contradicts. Evidence supporting different claims/obligations is genuinely different logical evidence, so it earns a distinctlogical_id. (Claimidentity already carries the candidatesubject+ obligationscope, so the supported claim ids differ per obligation.)apply_resolutionidempotent as a defensive net: if an evidence/claimlogical_idis already in the graph, reuse it instead of re-adding — a genuine duplicate can never again abort a whole run.Tests
Two synchronous regression tests in
test_sourcehunt_proof_investigation.pyreproducing the jsrsasign scenario (two candidates, same shared fact):test_evidence_identity_distinguishes_supported_claims— same kind/observations, distinct supported claims ⇒ distinct evidencelogical_id.test_apply_resolution_tolerates_duplicate_evidence— re-applying an identical resolution no longer raises.Verification
ruffclean on all changed files.@pytest.mark.asynciotests skipped becausepytest-asyncioisn't active in this venv — environmental, unrelated to this change.Branch naming
Named
fix/proof-hunt-eval-patches(not CVE-specific) intentionally — a landing spot for further proof-flow eval fixes surfaced by other CVEs.