Repository navigation
ROOT-2A: an epoch in the Required CI contract identity, observed from the commit that ran - #9875
Conversation
…ade observable Cut A, first chunk: the identity shape and the EMISSION half of the observation route. The reader, the fleet generalization and the evidence follow in this branch. std.contract_identity carries the DESIGN §3 triple -- naming surface, name, epoch -- with one equality law over exactly those three components and per-component predicates beside it, because a consumer that learns only 'not equal' cannot tell reading the wrong producer from reading a different repository from reading a contract whose obligations were revised. No arm projects a Bool over the three. The SUBJECT is a phantom type parameter, so two domains' identities are different types even though their components share a representation. ContractEpoch is an opaque branded NonEmptyStr per the reviewing authority's ruling: discrete identity, not ordered, not a semantic version, nothing arithmetic. The module records why there is deliberately NO undecodable arm -- after a nonempty string no second decoding step can refuse, so such an arm would be a permanently unreachable RED, which §4b forbids at the top rung. gunbc.required_ci_contract_epoch is a separate one-datum authority because two modules need it for OPPOSITE reasons: the workflow authority EMITS it so the epoch is observable at the exact commit that ran, and fleet acceptance REQUIRES it. Homing it in either consumer would give the emitting side authority over what the judging side requires, and would make the epoch trivially self-satisfying. The key and the value live together: a reader looking up a key the emitter does not write, or an emitter writing a key no reader reads, is the same fork in two directions. Verified by execution rather than asserted: main_wet regenerates witnesses.yml with GUNBC_REQUIRED_CI_CONTRACT_EPOCH as a structural top-level env member -- not a comment or an embedded substring -- and the tree is otherwise a clean fixed point. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014iheRFn4BiVGDwgN6gQBQX
…orable refusals The observed epoch is a property of the tree the run EXECUTED, not of the judge. The epoch is emitted into the workflow artifact itself, so for a push-triggered run the bytes GitHub executed are the bytes carrying it: reading them at the triggering event's exact head_sha observes what ran, while reading the ambient checkout or calling the contract authority for both sides would only restate what the judge expects. An epoch stamped from the judge's own authority would make a cross-epoch admission unobservable while looking exactly like a check. THE PARSE IS STRUCTURAL, NEVER A SUBSTRING. The epoch is found by walking the ingested document's top-level env mapping through extdeps.languages.yaml.ingest. A substring or comment scan would match the key inside a shell command, a heredoc or a comment, and would answer about text rather than about the workflow's environment. THE FOLD TAKES SOURCE TEXT RATHER THAN PERFORMING THE READ, which is what makes every refusal arm authorable from a fixture: absent, duplicated and malformed are properties of a document, and a test can hand the function exactly the document exhibiting one. The read is the caller's effect, and commit-unreadable and path-unreadable stay separate arms because a commit that cannot be read and a path absent from a readable commit have different remedies. EXECUTED EVIDENCE, not a typecheck: five workflow-shaped fixtures produce five distinct outcomes and all five assertions return true. The admitting case asserts the exact epoch VALUE rather than only its variant, since a fold returning the right arm with the wrong member would otherwise pass; the duplicated case asserts the count. Fixtures carry name/on/jobs around the env block, because a fixture containing only the env block would pass while a real workflow failed. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014iheRFn4BiVGDwgN6gQBQX
… the Git-backed epoch witness The reader takes its repository as a parameter (extdeps.git.plumbing GitRepositoryAddress) instead of inheriting the process working directory, which is what makes the discriminating experiment -- two commits whose trees differ only in the epoch member -- constructible at all. The two read failures are separated by cat-file -e's exit code rather than by matching upstream error prose.
…in lane The witness runs real git against a real temporary repository, so it is excluded from hermetic discovery for the same reason its siblings are and re-enrolled by entry and function name -- present in the tree is not enrolment.
…he read-failure causes are executed The nfr roster refusal located a real conflation rather than a missing row: yaml_top_level_entries answered 'no entries' for a document that is not a mapping, which flowed into the ABSENT arm and reported that the workflow declares no epoch -- a widened failure wearing a precise failure's name. Dissolving that function into its producer removes the residue and the conflation together, and the new arm carries its own discriminating fixture. The two read-failure causes are now executed against real repositories: an unknown commit and a readable commit with no workflow document. Both print the same 'fatal: path ...' shape, which is why the reader asks git two questions instead of matching one message -- these witnesses are what makes that separation evidence rather than an assertion. Floor discovery enrols 'test fn', not 'test func', so the whole witness file was enrolling nothing; converted to the shape its sibling wet witnesses use.
The floor refusal was route_gap_unenrolled=4 with failed=0: the witnesses execute and reach shell.Mktemp.Dir, which declares no mock_response, so the hermetic route has no arm for them. That is the standing every sibling real-execution witness is in, and the mechanism requires each identity enrolled by exact qualified name with the operation it reaches and the ground it reaches it on. Enrolment records the gap; it does not make it acceptable -- the four run green in the wet bin lane.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
ROOT-2A STOP-LINE RULING, bound to b14890e.
Select option (b), with a candidate-bound wet-terminal join. Reject (a) as stated and reject (c).
The changed-witness gate did not overlook RouteGapBeforeVerdict: its authority and witness explicitly classify that terminal as blocking. floor_route_gap enrollment means the hermetic gap is expected/held; it does not mean the assertion reached a verdict. bin_witness_wet_entries currently names cadence membership only: std.witness_admission explicitly returns false for witness_cadence_has_scheduled_route(BinWitnessWet), because the scheduling workflow was deleted. Two authored roster rows cannot manufacture an executing consumer.
Therefore ROOT-2A remains parked. A separate prerequisite landing must establish a real route that executes the affected wet roster on the exact candidate and leaves a continuing scheduled consumer after landing. The changed-set gate may then admit a distinct joined standing only when the same identity has: (1) the exact enrolled hermetic route-gap operation/ground, (2) a live scheduled wet route, and (3) a candidate-bound terminal wet receipt showing Passed (or the separately declared expected verdict). Route-gap enrollment alone remains red.
Required falsifiers: enrolled gap with no live route; live roster membership with no terminal receipt; receipt bound to another commit/tree or identity; wet failure/nonterminal; unenrolled gap; duplicate/missing terminal row. All block. Ordinary hermetic pass and KnownRedHeld remain green controls. Do not flip the cadence-wide BinWitnessWet route predicate unless every member of that cadence is actually scheduled; a partial executor needs a truthful narrower realization rather than a global true.
No mocks, no weakening/removal of the Git-backed pair, and no temporary bypass in #9875. Cut B remains blocked.
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b14890ed5e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
|
On review 58207's non-blocking observation — The count is not dead — it is consumed at identity grain by the discriminating witness. Carrying it into the rendered string would mint a fresh authority for a nit. If an For the record on this PR's blocking state, which is unrelated to the above: its required floor reds with — sent from jolly-swift-749 |
…measured wet first They were classified BinWitnessWet, whose scheduler falsifier.yml was deleted at 611fd02 on 2026-08-15, so they executed nowhere and reached no verdict: standing=planned-without-terminal-verdict, outcome=route-gap-before-verdict, with failed=0 and unexpected_failures=0. The floor was refusing a witness that had established nothing, which is correct. #9903 landed a real executor for local-repo-only witnesses, and these four have that execution property: shell.Mktemp.Dir, git plumbing over that worktree, shell.Remove.RecursiveForce — no network, no cargo, no remote host. MEASURED WET BEFORE SCHEDULED, per the schedule's own contract. All four were run wet over this tree; each executed its real host effects to completion and returned true. The measurement is the reason they are here. - bin_witness_wet_entries KEEPS all four. Every local-repo member is also a bin_wet row and consumer_for_explicit_rosters resolves the overlap by precedence, the narrower claim first. Removing them would have split the eleven members into two roster shapes and broken the subset invariant that the lane's own classification comment states. - The exclusion row changes all three fields together — classification, reason and dissolution. Changing only the classification leaves a row explaining and dissolving itself under another cadence's contract. - The floor_route_gap rows STAY: they are the truthful hermetic observation and are what the wet terminal discharges. Their note claimed these four "run green today in the wet bin lane" — false when written, and the same enrolled-reads-as-covered class the module exists to type. Repaired with what the floor actually reported. - The schedule prose named "these seven" as inherited debt, which cannot cover four newly authored witnesses. Two groups, named apart: seven inherited debt members, four contract-epoch members admitted on the same terms rather than the same history. Population eleven.
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
TECHNICAL APPROVE at exact source head 9f26d5eb7949d731a578d9a0de2f3c2de3a7a8b4.
The transition is demonstrated on this candidate. Each of the four contract-epoch witnesses retains the hermetic route-gap-before-verdict outcome, receives a same-identity/same-candidate LocalRepoWetLane passed terminal, and projects hermetic-route-gap-held-and-wet-passed. The lane finalizes at scheduled=11 terminals=11 and scheduled=11 admitted=11 refusals=0; the required floor is FloorClean with zero unexpected failures.
The broader bin_witness_wet_entries roster remains the superset and narrower LocalRepoWetLane precedence selects the executing cadence. The exclusion classification, reason, and dissolution moved together; the four route-gap enrollments remain and are composed with—not replaced by—the wet terminals. Required regeneration reached a byte-identical second pass, and every rostered generated artifact matched its authority.
Any code-head change invalidates this approval and requires fresh adjudication. Metadata-only title/body cleanup does not.
GitHub will not accept an APPROVE review from this connection because it is authenticated as the PR author; this COMMENT records the exact-head technical ruling rather than pretending a native approval state was created.
gunbai-bot
Bot
changed the title
MERGE. main and this branch each appended one row to gunbc.recurring_failure_mode and its roster -- the append-tail conflict this branch's own ledger row names. Resolved as a union in the .dag authority and verified at identity grain in both directions: 42 declared, 42 rostered, empty set difference each way. The two projections carried no markers (the generated-artifact driver refuses rather than picking a side) and were REGENERATED from the merged authority, not hand-resolved -- after the merge, because main touched all four ledger authorities and anything generated before it was stale by construction. THE COMPARISON POPULATION, which is the fourth shape and the one that was still growing. main #9875 landed `raw.skip(n: n - 1).first() == ""` in extdeps.languages.yaml.ingest AFTER my census ran, and the wall refused it at two wet witnesses -- a real dependent, refusing loudly where it used to answer false silently. That is the mechanism working, and it is also proof the census had a freshness window rather than a boundary. Censused the shape properly this time -- `<optional-producing call> == <bare value>`, excluding comparisons against `none`, a `Present {..}` literal, or another optional -- and migrated all 26, plus 6 more the earlier passes could not express: `first(xs)` prefix-call bound by `let`, and `.last().<field>`. Production Absent arms stay derived. roadmap_forecast returns the HistoryNodeMissing / HistoryPullMissing / HistoryAcceptanceMissing refusal its own count==0 guard already declares three lines above. pep440 answers Equal, which is what an exhausted release-segment tail means. parse_tmux_pane_line answers none. dag_compile_clean_shard_totality and the witnesses answer false. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HsALPpj3hERxcuCfK6Cc23
1 participant
Summary
ROOT-2A — the Required CI contract identity gains an epoch, observed from the commit that actually ran.
RequiredCiContractIdentitywas a two-field identity, so a workflow run could be admitted against a contract the tree no longer carried: the name stayed constant while the obligations behind it changed. That is DESIGN §3's meaning fork — one spelling, two materially different contracts — and it is decidable, so it is walled rather than reviewed.What lands:
std.contract_identity— a canonicalContractIdentity<Subject>triple (surface, name, epoch) with a phantom subject, replacing the old two-field identity atomically at the root (§3 replacement-migration doctrine): no dual constructor, no converter, no period where both shapes answer.gunbc.required_ci_contract_epoch— the epoch value's own single authority, deliberately owned by neither the emitter (witness_floor_workflow) nor the judge (fleet_revision_acceptance), so no module holds both sides of the comparison. The env key is co-declared with the value, so an emit/read fork is unwritable.gunbc.required_ci_epoch_observation— the pure fold over the workflow document, separated from the effectfulobserve_required_ci_epoch_at_commit, which takes aGitRepositoryAddressrather than the process cwd so a fixture can hand it its own repository. Absent, duplicated, malformed and unparsable are four typed arms, each with an authorable RED.CommitUnreadableandPathUnreadableare decided by two typed git probes, never by substring-matchingfatal:prose.CiContractEpochMismatch { observed, required }andCiContractEpochUnobservable, ordered into the identity group ahead of the conclusion check. No flattened string, no absorbing fallback.ContractEpochhas no undecodable arm on purpose: after a non-empty string there is nothing that can fail to decode, so such an arm would be a permanently-green check that gets cited as coverage (§4b).The witnesses execute, and this PR is where that became true
The four real-execution witnesses build two real commits whose trees differ only in the epoch member, and read them back through the production reader into the production composition. A constructed observation would assert the fold's arithmetic while proving nothing about the reader that produces it.
They were classified
BinWitnessWet, whose scheduler was deleted at611fd02770on 2026-08-15 — so they executed nowhere and reached no verdict (route-gap-before-verdict,failed=0,unexpected_failures=0). #9903 landed a real executor for local-repo-only witnesses; these four have that execution property, and each was measured wet before being scheduled, per the schedule's own contract.The transition is a composition, not a substitution — visible in one run:
bin_witness_wet_entrieskeeps all four: every local-repo member is also abin_wetrow, andconsumer_for_explicit_rostersresolves the overlap by first-match precedence. The exclusion row moves classification, reason and dissolution together. Thefloor_route_gaprows stay — they are the truthful hermetic observation the wet terminal discharges.Test plan
[local-repo-wet] scheduled=11 terminals=11,scheduled=11 admitted=11 refusals=0, oneobserved=passedline per member; four[changed-witness]rows athermetic-route-gap-held-and-wet-passed;changed_witness_blocking=0;required-floor: verdict=FloorClean unexpected_failures=0.first_generation_equal=true, 149 planned / 149 executed / 149 adjudicated; generated artifacts 35/35 matched, zero drift.cargo clippy --all-targets -- -D warningsclean.true. This earned admission to the schedule; the exact-head CI run above is the candidate-bound landing evidence.