Skip to content

XL-3 model-work: normative v2 semantic conformance — v1 is a probe, never the judge - #9672

Merged
gunbai-bot[bot] merged 13 commits into
mainfrom
session/sharp-deer-39
Aug 30, 2026
Merged

gunbai-bot[bot] merged 13 commits into
mainfrom
session/sharp-deer-39

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Aug 29, 2026 •

Copy link
Copy Markdown
Contributor

Merge standing

Schema landed; XL-3 gate not satisfied. This PR merges under the lean serial-gate standard as a fail-closed schema only — the XL-3 gate (native conformance execution over the real subject universe) remains ahead and serial. Confirmed by measurement on the final head:

  • No live Admitted/Complete/Active value: every production data row is the PartitionUnmeasured partition, prose notes, fixture source strings, or the authored exhaustiveness subject (a normative declaration, not a measurement); ConformanceAdmitted/OmittedArmHeld/PartitionMeasured/CoveragePopulationMeasuredComplete appear only in match arms and derivation-internal constructors.
  • No route consumes the authority: the two carriers are imported only by their own witness modules and the subjects module.
  • All successful fixture values are synthetic (fixture.* module paths, authored digests, a validating-constructor tree id).
  • No Symbol representation pinned (zero occurrences of Symbol across all six files; assertions are on source identity, never emitted bytes).
  • Required-gate enrollment, verified by identity: the witness modules are renamed under the test.claim.self_host_ seed prefix (they were declined_outside_gate_closure, 0 executed, before bc40f815689); the required-floor-disposition artifact of run 33289930448 (head 08b6d6d2c17) shows all three modules at 26 planned / 26 passed / 0 declined.
  • Post-merge rerun: with Refuse non-exhaustive imported coproduct matches #9676 (exhaustiveness repair) and Model the exact Symbol-to-Rust representation binding and eliminate bare String capture #9689 (Symbol authority) in the base, all 26 witness baselines re-ran green at merge head 683588c4d13; Model the exact Symbol-to-Rust representation binding and eliminate bare String capture #9689 touched none of this PR's imported modules (measured by diff), so no further rerun was owed for df20445537f.

Lane: XL-3 of the v1-bankruptcy program (#9664; chain XL-0 #9665 → XL-1 #9669 → XL-2 → XL-3 → XL-4 → XL-5). Gated MODEL-WORK ONLY until the manager releases the lane: carriers, an audit denominator, one authored subject, and executable witness fixtures. No transports, no corpus-wide measurement, no collision-zone or src/v1 edits.

What lands

gunbc.semantic_conformance — the normative carrier

  • Conformance, not equivalence. PrimarySemanticAuthority (AuthoredExpectedOutcome | AlgebraicLaw | MetamorphicRelation | RoundTripLaw | ExternalTargetContract) and SupplementaryObservation (V2EvaluatorObservation | LegacyV1Observation | PreviouslyRecordedOutput) are two disjoint types: BehaviorSubject.authority gives "the expected value is whatever v1 printed" no constructor — DESIGN §4b rung 4 for that class, ceiling and next-rung trigger stated honestly in supplementary_disjointness_ceiling_note (no permanently-green Bool witness is written for it, deliberately).
  • Subject identity is derived, not minted (manager ruling): BehaviorSubjectIdentity { retained_consumer, facet } keys the universe on XL-5's retained-consumer population × this lane's contract-facet axis. Effect operations are XL-1's std.primitive_projection PrimitiveIdentity — the receipt entry adds only the ordinal.
  • DifferentialRecord = binding + native-v2 + v2-evaluator + LegacyObservation (LegacyNotConsulted is a named state, not an absent optional) + ordered effect receipt (identity = operation × ordinal, so a positional re-alignment cannot absorb a reorder). Nine total dispositions via classify_differential_record; v1 is read only after the v2 routes decide, so deleting the legacy field can change nothing but LegacyV1Defect — witnessed as an invariance, not a sentence.
  • conformance_exit_gate reads numerator and denominator: CoverageStanding unmeasured ≠ measured-empty, so the gate cannot open over a roster nobody measured. Blocking set per brief; V2EvaluatorDefect tolerated only under EvaluatorOffPromotedRoute (route is an input, never a self-asserted row property).
  • ConformanceAdmission — the carrier XL-4's GenerationReceipt types against. Join key is source_tree: FloorDiscoveryTreeId (squash rewrites commits); source_revision: CommitSha rides as the informational head. The omitted-arm conjunct is typed and structural: ConformanceAdmitted carries OmittedArmTripleHeld only (fail-open unwritable there); ConformanceRefused carries the full OmittedArmVerdict, so a fail-open is a nameable refusal cause. The triple is derived by omitted_arm_triple — Held only on reject-with-identity / accept / reject-with-identity; every single-leg deviation (incl. reject-everything and wrong-identity) is FailedOpen with the direction named.

gunbc.semantic_conformance_subjects — first authored subject (manager-ordered)

Cross-module closed-coproduct exhaustiveness: provider/incomplete-consumer/complete-control/widened-provider fixtures as data, authority = the authored language contract, expected = refusal under infer_match_non_exhaustive. v1's known blindness on this shape (seed under repair in another lane) makes it the cleanest live demonstration of probe-never-judge. No differential record is authored — running the fixtures through the native acceptance path is the released lane's work.

gunbc.expected_value_authority_audit — the audit denominator

AuditRow (claim × ExpectedValueOrigin × AuditDerivationBasis), AuditPartition with the same measured/unmeasured structural split, refusals for origin-without-basis / duplicate identity / measured-with-zero-rows. Production value is PartitionUnmeasured, blocked_on naming the capability (a reference-closure relation; v2.lens.reference_deps as nearest producer). Deliberately not derived from v2.lens.vacuity — its EmitVsEval ⇒ ProvenIndependent arm is sound for operand duplication and is the exact forbidden sentence for semantic authority; consuming it would be the rostered authority_substitution class. Recorded in the module, before the first row.

Witnesses — 26 executable claims across three modules

Headliners: unanimous_agreement_on_a_wrong_value_is_not_conformance (all three implementations agree on a value the authority forbids ⇒ NativeV2Defect), legacy_observation_cannot_move_a_native_verdict, effect reorder / drop / extra ⇒ HostRealizationDefect (the extra-effect witness exists because a mutation control proved the drop witness could not make the length conjunct's RED reachable), anti-vacuity gate REDs, omitted-arm triple discrimination in every direction, fixture text discrimination for the exhaustiveness subject.

Execution evidence

See the evidence comment: 26/26 baselines TRUE at e99e1914229, four mutation controls each flipping exactly the targeted witness, byte-restore sha256-proven. CI green at 700561d0fbc.

Representation constraints

No Symbol representation pinned (measured: zero occurrences of Symbol across all six files): the carriers never name v2.std.node.Symbol or any Rust spelling of it, fixtures are .dag source text judged at source identity, and no witness asserts on emitted bytes — the schema is representation-agnostic with respect to the in-flight Symbol target-binding replacement.

What this PR does NOT do

No conformance verdicts about any real subject; no coverage areas marked measured; no v1 execution; no edits to v2.lens.vacuity, registries, emit_host, or src/v1 hand-Rust. The exit-gate emptiness required for cutover is a downstream measurement this PR makes stateable, refusable, and admissible — not one it claims.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj

gunbc-ci-auto-heal and others added 3 commits August 29, 2026 12:18
…ntary observation has no constructor into the authority position

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
…ns, BehaviorSubjectIdentity keyed on retained-consumer x contract-facet, ConformanceAdmission carrier for XL-4

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
gunbc-ci-auto-heal and others added 5 commits August 29, 2026 12:50
… join key, one type not three spellings)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
…Id beside informational CommitSha (squash rewrites commits; XL-4/XL-1 adopt the same pair)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
… RED is the exfiltration direction, exposed by a mutation control that failed to flip; drop the stray evidence script from the tree

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
…m conjunct typed on the admission (Held-only on the admitted arm, FailedOpen nameable on the refused arm, generation joined by tree id)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
… to the subject row it describes

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
@gunbai-bot

gunbai-bot Bot commented Aug 29, 2026

Copy link
Copy Markdown
Contributor Author

Witness execution evidence

Producer: ctrl-build --remote -- bash -lc 'bash ./xl3_witness_run.sh' (BuildBuddy runner; builds gunbc from the mirrored worktree, runs each witness via ./target/release/gunbc run --source-root dag --source-root src/v2 --entry <witness file> --function <fn>, reads the verdict from the Bool the ProcessExit refusal prints). Script content is reproduced below the results. Measured revision: e99e1914229. The one commit after it, 700561d0fbc, moves a §4c annotation only — zero semantic bytes.

Baselines — 26/26 TRUE

All 15 semantic_conformance_witness fns (incl. unanimous_agreement_on_a_wrong_value_is_not_conformance, legacy_observation_cannot_move_a_native_verdict, the omitted-arm pair), all 6 expected_value_authority_audit_witness fns, all 3 semantic_conformance_subjects_witness fns, and the extra-unexpected-effect witness.

Mutation controls — each with byte-restore (sha256 proven identical after)

mutation (applied to production carrier) expected flip observed
ExpectsValue arm made vacuous (any run satisfies) unanimous_agreement… → FALSE FALSE ✓
LegacyV1Defect made blocking legacy_divergence…never_blocks → FALSE FALSE ✓
length conjunct dropped from effect_receipts_agree an_extra_unexpected_effect… → FALSE, a_dropped_effect… stays TRUE FALSE / TRUE ✓
basis check inverted in audit_row_refusal_causes an_origin_claim_without_a_basis… → FALSE FALSE ✓

Finding from the mutation pass, recorded because it changed the diff: the first run of mutation 3 targeted a_dropped_effect_is_a_host_realization_defect and did not flip it — the containment join already refuses a drop, so the length conjunct's only reachable RED is an extra effect the authority never ordered. That gap became an_extra_unexpected_effect_is_a_host_realization_defect (commit ce236bb2d56); the re-run confirms the pair discriminates in both directions.

Prior runs

  • d1bf65c (pre-CommitSha/tree-id/subjects): 20/20 TRUE, mutations 1/2/4 flip, mutation 3 exposed the gap above.
  • The CI red at 18c209d was the NFR wildcard roster (fixed by explicit arms, 0800458c317); the red at e99e191 was a §4c trailing annotation (fixed by 700561d0fbc).
xl3_witness_run.sh (as executed)

The script builds once, prints TRUE/FALSE <fn> per witness by grepping the run's printed verdict, applies each mutation via a python string-replace on the production carrier, re-runs the targeted witness, restores with git checkout --, and ends by comparing sha256 of both carriers against their pre-mutation hashes.

🤖 Generated with Claude Code

https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj

@gunbai-bot
gunbai-bot Bot marked this pull request as ready for review August 30, 2026 03:00
gunbc-ci-auto-heal and others added 2 commits August 30, 2026 03:06
…_host_ seed prefix (they were declined_outside_gate_closure — 0 executed in CI)

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
…nti-pattern — delete them; their content already lives in (or moves into) leading annotations on the declarations they describe

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PRGCz8tWhRkSwcEhHoiZWj
@gunbai-bot

gunbai-bot Bot commented Aug 30, 2026

Copy link
Copy Markdown
Contributor Author

Both findings from review 57505 are fixed in 08b6d6d by deletion rather than conversion: each data …_note: String row duplicated a leading // annotation already standing beside it. supplementary_disjointness_ceiling_note — its unique content (the rung-4 ceiling and the compiler-refusal-harness next-rung trigger) moved into the leading annotation on SupplementaryObservation, the declaration whose disjointness it describes, and the EOF comment block went with the row (a trailing block with no following declaration is itself a §4c parse refusal). audit_instrument_substitution_note — the vacuity-lens/authority-substitution rationale was already carried in full by the module-top annotation ("WHY THIS IS NOT DERIVED FROM v2.lens.vacuity") and the no-DerivedFromVacuityVerdict-arm note on AuditDerivationBasis; the row was a straight duplicate and is deleted. Agreed the fixture source-text rows are data, not commentary — untouched.

@gunbai-bot
gunbai-bot Bot merged commit 38106f3 into main Aug 30, 2026
4 checks passed
@gunbai-bot
gunbai-bot Bot deleted the session/sharp-deer-39 branch August 30, 2026 03:34
gunbai-bot Bot pushed a commit that referenced this pull request Aug 30, 2026
) as typed evidence on the candidate's GenerationReceipt

GenerationReceipt { requirements, producer, subject, build, conformance_evidence: ConformanceAdmission, fallback }, joined on source_tree; the request carries it and the sole constructor records it. Seven causes name each way the evidence can fail to be about THIS candidate: refused, other tree, off the promoted route, omitted-arm failed open / unobserved / judged over another generation, and a candidate receipt whose requirements disagree with the parent binding. Fixtures derive every admission through admit_conformance + omitted_arm_triple, so the battery cannot author an admitted arm. effect_evidence stays absent by name until #9669's carrier is on main (the HOLD's reason). 34/34 green remote.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01A37WtqPwoQ1vj55d8yQMty
@briansrls
briansrls restored the session/sharp-deer-39 branch August 30, 2026 03:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

0 participants