Improve packet evidence selection quality - #1926
Conversation
|
Checkpoint: stage-0 proof-formula contract accepted (head unchanged at The typed-proof implementation now has an adversarially reviewed design contract: Notable contract decisions vs. the original handoff sketch:
Implementation started: stage 1 (pure proof-atom module in codestory-agent) and stage 3a (PHP producer: scope primitive, PHPDoc reader, foreach dispatch, construction) are in flight as isolated lanes. Next proof target: stage-1 module green + F1 adversarial review, then receipt plumbing (stage 2) with the Jekyll-only direct-packet gate. 🤖 Generated with Claude Code |
Typed obligation proof foundation (stage 1 of the obligation-aware evidence selector): a leaf module in codestory-agent holding the proof-atom concepts, the three shard formula groups, and a pure deterministic bounded role-unification matcher. Discharge inputs are verified source-aspect receipts and typed graph receipts only; all cross-receipt joins are node-identity joins; certainty gates are attributed per edge kind; absence facts require untruncated covering scans with traversal-kind evidence; coverage defaults to unknown and fails closed. Per-requirement verdicts run under one group-wide role assignment with fail-closed guards for non-self-standing subsets. Registered in the agent planning module allowlist with a leaf-ness assertion; no behavior change (nothing consumes the module yet). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Stage 2 of the obligation-aware evidence selector: flow requirements carry a proof spec (six shard requirements on the typed formula groups, everything else explicitly Legacy), and both production finalize sites build their receipt view through one shared filter that admits a strict subset of what evidence compilation retains. Formula-bearing requirements derive proof status exclusively from the proof-atom matcher; the name-token vocabulary path neither proves nor selects a public status for them, and remains authoritative for Legacy requirements bit-for-bit. After evidence compilation a reconciliation pass re-verifies formula-proven obligations against the compiled survivors and demotes fail-closed, then recompiles once — sufficient because support compilation never reads the plan and is idempotent on its own output, both pinned by tests. Pre-cap preview and capture receive an explicit anchorless view, so anchor-requiring atoms cannot discharge before atom-anchored verification exists. Proof verdicts are exported only through the env-gated step trace, with matcher aborts distinguishable from honest unproven verdicts. Jekyll guard verified: disposition supported with both site obligations proven through the Legacy path on the exact benchmark prompt. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Checkpoint: stages 1–2 landed — head
Both stages passed adversarial review (F1: two rounds — an unsound absence-scan arm and a per-requirement API gap fixed; F2: one round — a name-token predicate could still select the public status level on the non-Proved path, now always Unsupported). Jekyll guard verified on the exact benchmark prompt: disposition Process note for future gates: the harness exits 0 even when cache prep fails — verdicts are read from rows and direct packet inspection, never exit codes; and the embedded-model build uses 🤖 Generated with Claude Code |
Stage 3 of the obligation-aware evidence selector, three producer waves verified against their real-target indexes: PHP: a scope-visibility primitive, a PHPDoc list<T>/T[] element-type reader, foreach element binding through the manual receiver-call engine (one combined loop-element marker carrying the exact foreach range so iteration and callsite containment are same-receipt facts), and constructor call receipts from object-creation sites with same-namespace resolution. The marker registry becomes a list-valued family table. C#: a manual type-usage channel gated on binding tables and stamped certain producer-side (pending edges finalize against unique same-root declarations before the index publishes; uncertain edges never discharge), primary-constructor parameter types, constructor-body and chained-creation receiver calls with class-anchored sources, and a same-root-namespace declaration arm in call resolution. CSS: the structural collector reparses with comment/string blanking; import statements become MODULE nodes with real spans and file-to-file IMPORT edges resolved to canonical file identities; custom properties mint only at declarations; selectors only in selector position; keyframes become FUNCTION nodes; selector-to-keyframe and selector-to-custom-property usages resolve across the bidirectional import-graph component with ambiguity failing closed. All producers fail closed on hostile shapes; unrelated-edge counts are invariant against unpatched baseline indexes on the reference targets. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
|
Checkpoint: stage 3 producer wave landed — head Three language producers, each accepted only after its real-target index oracle matched exactly (fixture suites alone were provably insufficient — every wave failed its first oracle on a shape the fixtures missed, and the misses were all general-language semantics, not benchmark tuning):
Review trail in 🤖 Generated with Claude Code |
Decision point after gate round 6 — full picture and a recommendationCommitted and green: Uncommitted: stage 4 (admission, retention, protection, anchored verification, selection) — ~2,000 production lines, nine files, independently verified at runtime 909 / agent 307 / contracts 44, F3-reviewed with its blocker fixed. Gate status (four-packet direct gate):
Six rounds eliminated, in order: trail fan-out burning the retrieval stage clock; per-query promotion state with no cross-query bootstrap; unfiltered promotion mass-displacing base evidence; need-set flooding from generic membership/usage patterns; three environmental cache-provenance traps that made rounds 1–4's A/C numbers invalid measurements (documented in What remains is formula discrimination, not a bug. Admission priority by atom-role multiplicity is in flight and should close AutoMapper. For Animate, C4 treats every animation source as interchangeable while the manifest expects two specific ones — admission cannot fix what the formula accepts, and I deliberately declined to add an import-order preference to make the benchmark's two files win; that would be fitting the benchmark. Recommendation: commit stage 4 to keep the reviewed work safe, keep this PR draft, and take the C-formula expressiveness question to a scoped contract review rather than a seventh admission round. Full analysis with options in The exact-agent A/B has NOT been run and will not be until all four packets pass — that gate is exactly why three prior candidates produced worthless numbers. 🤖 Generated with Claude Code |
Stage 4 of the obligation-aware evidence selector, plus a matcher correctness fix. Admission: candidate resolution becomes a re-prioritizable queue whose promotion is gated on identities a still-unproven material atom needs, restricted to the cross-container kinds whose endpoints name retrieval-underranked containers, bounded by atom-derived per-role slots, and prioritized by how many role positions an identity fills. Identities accumulate across a packet's queries so a chain can bootstrap from the one container that ranks naturally. Retention hydrates atom-required edge kinds off the retrieval stage clock, over retained candidates, recording per-trail coverage whose enumerated set is narrowed to what its own absence claim needs. Protection reserves the carriers and edges partially matched atoms require, verification anchors its windows at receipt-carried lines, and the public typed-support allow-list carries the kinds atoms discharge. Matcher: when a requirement group cannot prove as a whole, its requirements are now attempted most-constrained-first rather than in declaration order, so a weakly constrained requirement can no longer capture a shared role and force its stronger sibling onto wrong bindings. Gate status, honestly: the Monolog and Jekyll packets pass the direct gate; the AutoMapper and Animate packets do not. Their remaining loss is downstream of admission — both AutoMapper endpoints are admitted and resolved, then dropped by the citation cap while a weaker binding holds the protection. No agent A/B has been run. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Stage 4 landed as
|
Status
Draft quality lane based on the proven 0.17.0 checkpoint now on
dev/codestory-next. The branch currently contains four accepted bounded improvements; obligation-aware proof/selection work remains in research and is not yet implemented.Current source
ccebbe622decb84b20b5c04dd66a26ed4f9a150e37c437607ec1ac77396770118a58c3235df3cc838173044227c012b95a5d409037f14a5e27826ca8Already on this branch
Next architecture
Move semantic proof authority from name-shaped citation predicates to typed proof atoms over verified source aspects and typed graph receipts. Retrieval queries remain provenance only. Reuse existing retrieval, graph, source-read, cap, drill, and fail-closed machinery.
Do not add repository vocabulary, prompt-token proof heuristics, quoted-path reconstruction, global top-k/ranking changes, or embedding changes.
Gate
Direct exact-binary packets must pass Monolog, AutoMapper, Animate, and the Jekyll guard before any exact-agent A/B. Reuse unchanged baseline rows. Commit only a candidate that improves the affected exact-agent shard without a material latency or reliability regression.
Closes #1925
Refs #1179