Add the evidence-intake contract: external suppliers behind profile authority - #20
Merged
Conversation
…uthority The probe-supplier surface opens: an external tool (fuzzer, proof worker, observation plane) submits evidence rows through an intake document, and correctful validates, binds, combines, and applies policy without becoming every probe runner. An adversarial pre-implementation design review reshaped the draft; its five critical findings are the design: - Authority lives in an invoker-owned profile (name, mechanism, max tier — the external Runner.MaxTier), never in the row. - Outcomes are an enum: verified / counterexample / inconclusive / not_run / error. Only a counterexample refutes — an unproved proof or a fuzzer timeout is not a refutation (the t.Skip lesson, applied at the contract boundary). - Subject identity is head SHA plus input digest, both required; a mismatch rejects the whole document as stale, disclosed. - A required supplier with no admitted document blocks the gate; rejected rows keep identity, outcome, and reason — a rejected counterexample can expose claim drift and stays visible. - Ambiguously anchored claims reject rows; every admitted row carries binding "supplier-attested" and an [external: …] marker on verified AND refuted rows — the receipt never launders supplied trust. Probe ids are namespaced by construction (ext:<supplier>/…), decoding is strict, paths must be regular files outside the repository tree, all external strings are control-stripped and bounded, and the admitted document's SHA-256 is the audit pin. Policy mechanisms opened from an enum to a token shape so floors can require supplier mechanisms — a typo fails closed as an unsatisfiable floor. Receipt.GateBlocked is now THE gate definition shared by main and the renderers' exit-gate line, which the text receipt now prints too. Schema 0.0.12. Live-verified on this change: admitted document → T4 verified row with external marker and gate green; counterexample row → refuted, marked, blocked; missing required document → blocked with the reason on the intake line. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp
correctful receipt30 claims — ✅ 30 verified · ❌ 0 refuted · Change:
|
| Tier | Claim | Statement |
|---|---|---|
| T1-assertion | TestConfigValidatesLoudly |
Config Validates Loudly |
| T1-assertion | TestInTreePathsRejected |
In Tree Paths Rejected |
| T1-assertion | TestAdmissionGates |
Admission Gates |
| T1-assertion | TestAuthorityComesFromTheProfile |
Authority Comes From The Profile |
| T1-assertion | TestOutcomeVocabulary |
Outcome Vocabulary |
| T1-assertion | TestRowRejections |
Row Rejections |
| T1-assertion | TestLoadValidatesAndDigests |
Load Validates And Digests |
| T1-assertion | TestPatternMatching |
Pattern Matching |
| T1-assertion | TestEvaluateFloors |
Evaluate Floors |
| T1-assertion | TestEvaluateScopeFloorAndLLMGate |
Evaluate Scope Floor And LLMGate |
| 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 |
| T1-assertion | TestReceiptCarriesToolVersion |
Receipt Carries Tool Version |
| T1-assertion | TestPolicySectionRenders |
Policy Section Renders |
| T1-assertion | TestIntakeRendersAndExternalMarks |
Intake Renders And External Marks |
Harvest coverage: 11 files — 4 claimed · 7 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.12 · correctful v0.0.0-20260818010406-1e80bcc64651 1e80bcc · 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.
Opens the probe-supplier surface. An adversarial pre-implementation design review reshaped the draft contract; its five critical findings became the design: invoker-owned profile authority (the external
Runner.MaxTier), an outcome enum where only a counterexample refutes, exact subject identity (head SHA + input digest), required-supplier gate blocking with visible per-row rejections, andsupplier-attestedbinding markers on every acting row. Probe ids namespaced by construction; strict decoding; out-of-tree regular files only; audit pin via document digest.Receipt.GateBlockedbecomes the single gate definition. Schema 0.0.12. Live-verified: all three gate legs behaved to spec on first run.🤖 Generated with Claude Code
https://claude.ai/code/session_015GeUG1gboWiZSnFyzQghyp