Bind LLM-proposed claims to changed tests behind two mechanical gates - #13
Merged
Conversation
The model may now name, in an optional "test" field, a changed Go test
that checks its proposed claim — but the edge only counts after two
machine checks, because a wrong claim→test association plus a passing
test would mint exactly the false verification this tool exists to
prevent:
1. Existence, at mint time: the test's definition must appear in the
diff the model was shown (added or context line of a changed
_test.go; deleted definitions don't count), exactly one changed test
file may define it, and the claim's file must be shipped Go code.
A failed edge mints the claim probe-less, as before.
2. Execution, at run time: the probe run is instrumented, and the pass
counts only when the coverage profile shows execution reaching the
claim's file (binding "file-covered"). A profile that never touched
the file refutes the edge ("file-not-reached"); no profile at all
raises nothing. Both discards are disclosed on the remainder row.
Refutation keeps unconditional dominance — a failing test blocks the
gate no matter whose edge bound it; a mis-attributed refutation is
fail-safe because the failure is real. Verified rows now carry the
[llm-proposed] marker in both renderers, so verification never launders
the provenance away. Schema 0.0.8; binding vocabulary moved to named
schema constants.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp
correctful receipt33 claims — ✅ 33 verified · ❌ 0 refuted · Change:
|
| Tier | Claim | Statement |
|---|---|---|
| T1-assertion | TestExtractMintsValidatedProposals |
Extract Mints Validated Proposals |
| T1-assertion | TestFenceWrappedOutputTolerated |
Fence Wrapped Output Tolerated |
| T1-assertion | TestProseWrappedOutputFailsLoud |
Prose Wrapped Output Fails Loud |
| T1-assertion | TestAPIErrorSurfaces |
APIError Surfaces |
| T1-assertion | TestByteCapIsHardAndDisclosed |
Byte Cap Is Hard And Disclosed |
| T1-assertion | TestContextCancellationPropagates |
Context Cancellation Propagates |
| T1-assertion | TestSectionFileParsing |
Section File Parsing |
| T1-assertion | TestDotDirSectionsNeverReachTheModel |
Dot Dir Sections Never Reach The Model |
| T1-assertion | TestGithubSectionsIncludedAfterCode |
Github Sections Included After Code |
| T1-assertion | TestGithubSectionCannotCrowdOutCode |
Github Section Cannot Crowd Out Code |
| T1-assertion | TestLLMEdgeExistenceGate |
LLMEdge Existence Gate |
| T1-assertion | TestLLMEdgeFlowsThroughHarvest |
LLMEdge Flows Through Harvest |
| T1-assertion | TestParseCoverProfileRealShape |
Parse Cover Profile Real Shape |
| T1-assertion | TestCoverageProvenBinding |
Coverage Proven Binding |
| T1-assertion | TestFileBindingFor |
File Binding For |
| T1-assertion | TestLLMEdgeFileBinding |
LLMEdge File Binding |
| T1-assertion | INV-001 |
Remainder Contains Every Unverified Claim |
| T1-assertion | INV-002 |
Refuted Claim Never Enters Remainder |
| T1-assertion | TestVerifiedClaimCarriesProbeTier |
Verified Claim Carries Probe Tier |
| T1-assertion | INV-007 |
Refutation Dominates Verification |
| T1-assertion | TestT0PassConfersNoVerification |
T0 Pass Confers No Verification |
| T1-assertion | TestScopeExclusionsAndInputDigestAreDisclosed |
Scope Exclusions And Input Digest Are Disclosed |
| T1-assertion | TestSuppressedMentionsAreDisclosed |
Suppressed Mentions Are Disclosed |
| T1-assertion | TestRemainderSectionAlwaysRenders |
Remainder Section Always Renders |
| T1-assertion | TestCoverageDisclosesUnreadFiles |
Coverage Discloses Unread Files |
| T1-assertion | TestUnreadCausesRenderSeparately |
Unread Causes Render Separately |
| T1-assertion | TestAnchoringSummaryAndMarkers |
Anchoring Summary And Markers |
| T1-assertion | TestLLMProposedMarker |
LLMProposed Marker |
| T1-assertion | TestRefutedDetailComesFromFailingProbe |
Refuted Detail Comes From Failing Probe |
| T1-assertion | TestReceiptSanitizesPathsAndPinsSHAs |
Receipt Sanitizes Paths And Pins SHAs |
| T1-assertion | TestDetailSanitizationIsCategorical |
Detail Sanitization Is Categorical |
| T1-assertion | TestLLMPassCountsOnlyWithConfirmedEdge |
LLMPass Counts Only With Confirmed Edge |
| T1-assertion | TestLLMVerifiedRowKeepsProvenance |
LLMVerified Row Keeps Provenance |
Harvest coverage: 11 files — 5 claimed · 6 scanned · 0 unread
2 spec-id mention(s) not minted as claims — the repo defines no spec-id corpus, so a reference has no possible referent
schema 0.0.8 · exit gate: refuted claims block; the remainder informs, never fails
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.
Closes the extract→bind→verify loop for the LLM path without giving the model certification power. The model proposes an EDGE (an optional
testfield naming a changed Go test); two mechanical gates decide whether it counts:_test.go. Deleted definitions do not count. An ambiguous name (defined in two changed test files) fails closed. The claim's file must be shipped Go code.binding: file-covered).file-not-reachedrefutes the edge; a missing profile raises nothing. Both discards are disclosed on the remainder row.Refutation keeps unconditional dominance. Verified rows keep the
[llm-proposed]marker in both renderers. Schema 0.0.8.🤖 Generated with Claude Code
https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp