docs: withdraw the "9 unattributed object branches" claim — a vocabulary mismatch, not a finding - #279
Open
avrabe wants to merge 1 commit into
Open
docs: withdraw the "9 unattributed object branches" claim — a vocabulary mismatch, not a finding#279avrabe wants to merge 1 commit into
avrabe wants to merge 1 commit into
Conversation
…vocabulary mismatch, not a finding I read a reconciler's vocabulary as a finding about the object, committed it as evidence, and filed it upstream as synth#944. It was wrong. synth reproduced the exact 9 keys from the manifest + provenance map committed in this repo and showed every one is a provenance entry for a REAL SOURCE WASM OP: 6 preserved br -> unconditional branch 3 folded-predication select -> predicated IT-move, no branch at all None is a miscompile; none is an unattributed compiler-introduced branch. witness's manifest records only br_if / br_table_target / br_table_default / if_then / if_else — it never instruments unconditional br or select, CORRECTLY, because they are not decisions. `only_in_synth` means "synth entry with no WITNESS branch record", and its hardcoded text "(object branch witness never instrumented)" is literally accurate while reading as an alarm. So the claim this repo carried — "Those 9 are new object-code obligations: control flow that exists in the shipped binary and in no source or WASM decision, so no source-level MC/DC argument can discharge them." — is withdrawn. The correction is inline where the claim was, not appended elsewhere, and the "does NOT establish" bullet that repeated it is struck through rather than deleted so the record shows what was believed and why it changed. The mpu-thin (12) and const-init (4) counts get the same treatment: same category, not unexplained obligations. Fixed upstream in synth v0.57.0 (#967), which now emits verified machine-readable origins for genuinely compiler-introduced branches — so the category that DOES need discharging is populated and named instead of inferred from a count. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo
Codecov Report✅ All modified and coverable lines are covered by tests. 📢 Thoughts on this report? Let us know! |
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.
I read a reconciler's vocabulary as a finding about the object, committed it here as evidence, and filed it upstream as synth#944. It was wrong, and synth v0.57.0 (#967) settles it with data from the very manifests committed in this directory.
What they found
Reproducing the exact 9 keys from
switch-thin.{witness,provenance}.json, joined the waywitness object-dispositiondoes, every one is a provenance entry for a real source WASM op:preservedbrfolded-predicationselectNone is a miscompile. None is an unattributed compiler-introduced branch.
witness's manifest records only
br_if/br_table_target/br_table_default/if_then/if_else. It never instruments unconditionalbrorselect— correctly, because those are not decisions. Soonly_in_synthmeans "synth entry with no witness branch record", and its hardcoded text — "(object branch witness never instrumented)" — is literally accurate while reading as an alarm.What this PR changes
The claim this repo carried:
is withdrawn. The correction goes inline where the claim was, not appended elsewhere, and the "What this does NOT establish" bullet that repeated it is struck through rather than deleted — so the record shows what was believed and why it changed. The mpu-thin (12) and const-init (4) counts get the same treatment.
The mistake worth naming
The join was doing exactly what it documented. I supplied the alarming interpretation, and the number was large enough to look like a finding. The tell I missed:
only_in_synthis a reconciler category — it describes a relationship between two tools' records, not a property of the object. A count that only exists because two tools instrument different things is a vocabulary mismatch until proven otherwise.Upstream outcome is genuinely useful though: synth v0.57.0 now emits verified machine-readable origins for branches it really does introduce, so the category that does need discharging is populated and named rather than inferred from a count. That is a better state than before I filed it — but the claim in this repo was still wrong, and it was wrong on
main.Related: this is the second correction to this document (the first marked per-file attribution provisional pending witness#179). Both were caught by upstream reproducing our committed artefacts, which is an argument for committing the raw manifests rather than only the rendered rollups.