Repository navigation
Conversation
ListHeadEmpty/ListHeadNonEmpty are not list_head variants; the wrong names caused parse/typecheck failure in the witness corpus. Co-authored-by: Cursor <cursoragent@cursor.com>
Heal could not auto-push workflow paths; commit the emitted ci.yml with the all-seven partition crate check step and timeout bump. Co-authored-by: Cursor <cursoragent@cursor.com>
gunbai-bot
Bot
force-pushed
the
session/sharp-fox-403
branch
from
August 6, 2026 03:25
673e455 to
b6b55a8
Compare
Regen emits sorted derived membership for std-core; sync committed stage0 output so regen --verify stays at divergence zero. Co-authored-by: Cursor <cursoragent@cursor.com>
…nt) (#7876) * WIP: blackwell * Typed LLM attempt receipt: counts and durations stored, every rate derived First slice of the local-inference economics lane. Lands the receipt carrier that makes the hardware question measurable, in the observing product layer (DESIGN external-upstream-decomposition: extdeps.llm.* owns provider wire contracts, this owns what WE observed when we ran something). Mechanism: - TokenCount instantiates the std.measure Count axis (HardwareThreadCount / CharacterCount precedent), declared here not in std.measure because an LLM token is domain vocabulary and std/measure.dag is seed-emitted. - No throughput, rate, or cost field exists in the record. Tokens-per-second and accepted goodput are DERIVED as exact FieldOfFractions<Nat> over the same authority gunbc.econ.acquisition ConversionRate consumes; the floor projection is a declared lossy view, total by typed refusal. - Usage is three-valued: an attempt whose provider reported no usage is not an attempt that consumed nothing. Missing usage refuses the economic derivation without refusing the attempt or its disposition. - Goodput counts ACCEPTED dispositions only, so a host that doubles token rate while halving acceptance shows no gain. - Admitted sessions and active sequences are separate observations; a server sustaining four sequences can admit considerably more sessions. - SubstrateIdentity binds the compiler revision, because escalation rate is endogenous to both the model improving and gunbc needing less judgment. Evidence: 13 witnesses green by execution, incl. RED controls for zero and absent decode duration (no fabricated throughput), unobserved usage, empty roster, and zero observation window. Honest limits recorded in-carrier, both measured rather than assumed: - TokenCount is structurally identical to HardwareThreadCount, so it buys reading clarity, not a construction wall. - Requested/resolved model brands do NOT wall substitution. A scratch probe passing RequestedModelIdentity into a ResolvedModelIdentity parameter resolved and ran green. An earlier draft of the note claimed a typecheck refusal and cited a witness that was never written; both were false and are retracted in the carrier with the next-rung trigger named. No cost derivation lands here: the token-rate rows are not yet cited, and fabricating a rate to make the arithmetic run is what the follow-on prevents. This slice declares its frontier rather than claiming a production consumer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: local inference * Re-home TokenCount onto std.measure (review 48816): consume the family, don't fork it review 48816 found the merge-blocking defect and was right. TokenCount was declared locally in gunbc.econ.llm_attempt_receipt as Measure<Count, One, Nat>, citing extdeps.pricing.billing_units as precedent for downstream placement. Verified against the tree, the citation does not cover it. The billing_units aliases introduce their own phantom markers (PerStoredUnitMonth et al), so MoneyRate<PerStoredUnitMonth> is a genuinely new point in the type space that cannot be written in std without importing vendor vocabulary. Measure<Count, One, Nat> takes only arguments std.measure already owns, and that module already names the shape three times: HardwareThreadCount, CharacterCount, AmortizationMonths. A local fourth name was therefore a DESIGN section 3 fork, not a downstream instantiation. The review offered a tracked deferral as an alternative. Not taken: the only argument for deferring was the seed-regeneration cost, which is the cost of doing this correctly rather than a reason to avoid it, and deferring for the author's convenience is the unmarked-workaround shape DESIGN section 5 names as a line-stop signal. - TokenCount, token_count, token_count_value now live in dag/std/measure.dag beside their three siblings, under token_count_note, which records the billing_units distinction so the reasoning is not rediscovered, and repeats the siblings' honest limit: all four are structurally identical, so the family buys reading clarity and one construction site each, never a wall. - llm_attempt_receipt consumes them and retracts the bad citation in llm_token_count_authority_note. - src/v1/stage0/src/std_measure.rs regenerated (seed-emitted module). Evidence: regen_stage0 wrote 132 generated files with exactly one changed; the regenerated seed compiles; regen_stage0 --verify reports regen_divergence_count=0 with a binary rebuilt FROM the new seed, so the self-host fixed point holds rather than being self-confirmed by a stale seed. All 13 witnesses re-run green against the std-homed carrier. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Fix stale symbol citation left by the previous rename (review 48829) llm_model_identity_brand_note cited llm_token_count_placement_note, which the tree no longer contains: the previous commit renamed that note to llm_token_count_authority_note while re-homing TokenCount, and the honest-limit claim the sentence points at moved to std.measure token_count_note. Verified as dangling — the citation was the only occurrence of the name anywhere in dag/. Now cites std.measure token_count_note, where the Count-axis family's mitigatable-rung limit actually lives. This is the DESIGN section 3 stale-citation class in a note whose own subject is a false citation, and it is the failure mode that rule predicts: a rename invalidated a name-level reference with nobody touching the referring line. A symbol citation is at least decidable by grep, which is how review 48829 caught it; the positional form would not have been reachable at all. Swept the rest of both files for the same defect rather than fixing only the reported instance: dispatch_execution_receipt_bar_note, token_count_note, llm_token_count_authority_note, llm_attempt_receipt_frontier_note, ConversionRate, FieldOfFractions, character_count_note, HardwareThreadCount, CharacterCount, AmortizationMonths, dispatch_usage_unobserved, DispatchUsageObserved, MoneyRate and PerStoredUnitMonth all resolve. Witnesses re-run green. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: local inference * HOST-0: program-scoped host assimilation, replacing the global host x spine cross-product Two DGX Spark inference appliances (srv5, srv6) are on order. Enrolling them against the current model would manufacture obligations they can never satisfy: host_standup_spine is ONE universal list -- BMC credential convergence, virtual-media OS install, Actions runner slots, build cache, green-place pinning -- and host_phase_status crossed every enrolled host with all of it. An appliance has no BMC and no runner user, so those cells could never be converged and could never honestly be marked so. A completeness number computed over invented obligations is worse than no number. The correction is program scoping, NOT an Applicable | NotApplicable verdict. A verdict arm would keep the false cells and label them -- the parallel representation shape (DESIGN section 3) -- and leave every consumer to remember to filter. Participation now SELECTS which obligations exist, so an obligation that does not apply is not a labelled cell, it is not a cell. - New gunbc.host_assimilation_program: FleetParticipation (CiRunner | InferenceServing), HostEnrollmentIntent, HostAssimilationProgram, assimilation_program_for. Participation is a LIST because the axes are independent, and it is a role rather than a hardware kind, so a future Altra dedicated to serving does not inherit BMC obligations from what it is made of. - Phase-to-participation classification is an EXHAUSTIVE match over both closed phase enums, so a newly added phase cannot silently default into or out of a program -- it does not compile until classified. Construction, not validation. - It lives in the new module rather than as a field on HostStandupStep: that would reshape fourteen rows in load-bearing host_standup.dag, and that module's own gap-ledger note already ruled its row-reshaping change stays separable. - The program is DERIVED by filtering the spine, never a second hand-authored step list that could drift. - host_phase_status is enrollment-driven; the global-spine path is DELETED, not retained beside the new one. fleet_subsumption_hosts is now a projection of fleet_subsumption_enrollments, so consumers that only care which hosts exist are untouched and the two lists cannot disagree. Evidence, green by execution (12 witnesses on the refactored module): - IDENTITY: a CI enrollment selects the whole spine, and the runner-fleet matrix is still hosts x spine. Every pre-existing regression witness passes unchanged -- no-producer-is-UnknownRefused, the absorbing-fallback RED control, the reconcile upsert/teardown/noop diff, observation coverage, remaining work. - SCOPING: an inference enrollment carries zero BMC/runner/build-cache/ green-place/session-placement cells and exactly the four shared obligations. - TOTALITY: no spine step is unclaimed by any participation. - Downstream consumers re-run green: host_swap_backing, host_network_diagnosis, host_toolchain_components. Prefix phases are CI-runner only, deliberately. A Spark has real arrival obligations, but they are its own and get authored where that arrival is modeled; inheriting a differently-shaped host's provisioning steps because they sound generic is the exact false-obligation defect this removes. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Canonical participation projection: program identity is set-semantic, not list-shaped HostEnrollmentIntent.participation has set semantics -- step selection asks only whether SOME participation claims a step, so order and duplicates were already invisible to which obligations exist. Identity did not agree: it joined the raw list, so [Ci, Inference], [Inference, Ci] and [Ci, Ci, Inference] selected identical steps while deriving three different identities -- a second representation of one program (DESIGN section 3). Identity now projects through a fixed canonical roster filtered by membership, so a duplicate or a reordering cannot reach it by construction; there is no canonicalization step for a caller to forget. Roster completeness is the residue construction cannot remove, so it is walled by an exhaustive match (fleet_participation_in_canonical_roster): a new participation does not compile until stated, and its witness reds if stated but omitted from the roster. Green by execution, 10 witnesses. The discriminating control pins identity to independently authored literals -- the duplicated enrollment must derive "ci-runner+inference-serving" and must NOT derive "ci-runner+ci-runner+inference-serving", which is exactly what the replaced derivation produced -- so the repair is falsifiable rather than satisfied by any constant-returning function. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
string_contains is a std primitive, not exported from v2.std.text. Wrong imports caused compile-clean failures on the partition witnesses. Co-authored-by: Cursor <cursoragent@cursor.com>
* WIP: local inference * REVIEW-0 (wip): std.judgment kernel; grounding_ledger recut onto it; retire stale ctrl consumer claim Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * WIP: local inference * Fix three compile defects in the judgment kernel recut All three were mine, all in code described as done before it was executed: - the three ReviewDecision helpers took a bare ReviewDecision with no type arguments (compile-clean: expects 3 type arguments, got 0); parameterized them to match the std.change generic-fn idiom - grounding_ledger imported DeclarationRef/WholeDeclaration from std.types, where they do not live; the module originally carried no imports at all, since bare references resolve through the containment tree - residue_forced_decision's if branches did not unify (alias GroundingDecision vs bare ReviewDecision coproduct); both arms now go through typed constructors Green by execution, 6 witnesses, against the ledger test's small closure. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Back out std.judgment: it re-mints std.claim_evidence Operator ruling. std.claim_evidence already models this: Claim<S,T,P,Scope,Bound> for the criterion and its bounded subject, RecordedFact<F> for evidence input, EvidenceLink for direction/inference-rule/authority/provenance/freshness/ fidelity/independence, EvidenceInference for applicable-vs-insufficient, ClaimRequirementReadiness for ready/missing/challenged/conflicted/refused, and ClaimReadinessReceipt over a required claim population. It has a production-shaped consumer in gunbc.source_integration_landing_spine. JudgmentAuthority + ReviewDecision collapsed distinctions that authority already preserves -- support vs challenge, both at once, evidence-missing vs evidence-rejected, inference rule vs authority vs provenance, freshness, fidelity, independence. The module's own note claimed provenance was the shared fact; provenance already had one home. I did not DFS far enough before minting. Two further defects in the deleted design, recorded so the recut does not repeat them: JudgmentAuthority mixed orthogonal axes (rule, execution attempt, actor, evidence container -- an operator judgment arriving via an external artifact inhabits three at once), recreating the provider-enumeration defect one level up; and judgment_is_reached was described as a clearance conjunct, which is unsafe -- a reached judgment may be 'this field is anemic', and a judge confirming every violation would show total decision coverage and zero clearances. Those must never share a function. grounding_ledger and its test are restored to main pending the claim_evidence recut. The retired ctrl consumer claim is kept: it was independently verified. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> * Retire stale ctrl consumer claim from anemia eval corpus README The README asserted the corpus was consumed cross-repo by ctrl's coherence gate. Verified false: the only occurrence of that relationship in the tree was the sentence asserting it, and ctrl/ is being deleted. A named consumer existing only in the prose describing it is not evidence of execution. Two adjacent citations corrected in the same paragraph: - PR #5302 was described as 'not yet on main', which reads as pending. Verified CLOSED, never merged, 2026-06-19 -- it is a historical proposal, not a queued one. - 'the corpus remains valid' overstated it. Its own README says inputs are reconstructed rather than rebound against the current tree, so it is a fixed historical decision-eval; useful ground truth, not evidence of live coverage. States the durable fact -- no current consumer -- rather than inheriting a moving project status or naming a future slice that does not exist symbolically. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> --------- Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com> Co-authored-by: Claude Opus 5 (1M context) <noreply@anthropic.com>
Derive unit membership via module_dag_forward_closure directly instead of stage0_module_dag/partition_unit_members (stack overflow at witness). Include stage0 partition compile gate timeout in ci_workflow witness backstop step-sum receipt. Co-authored-by: Cursor <cursoragent@cursor.com>
Contributor
|
Operator ruling (still-bat-561): split into C1/C2/C3. C1 (all-seven compile gate) continues on #NEW — this combined draft is closed to avoid duplicate lanes. C2 closure + C3 oracle will follow after #7908 lands. |
4 tasks done
Contributor
|
C1 continuation: #7925 |
Contributor
|
Superseded (operator still-bat-561, msg_88e9e903): C2 and C3 now exist as fresh lanes from
C1 shipped separately as #7925. This combined draft stays closed. — sent from sharp-fox-403 |
Contributor
|
Closing as superseded. The combined C1/C2/C3 partition branch has been split into three focused lanes, all of which now exist:
Nothing from this branch is being lifted. Its emitted-reference oracle carries two known weaknesses — an empty-observation narrow and text scanning — and the empty-observation narrow is disqualifying rather than merely weak: zero observations trivially satisfies both 'no extra observations' and 'no duplicate observations', so those properties pass vacuously exactly when the instrument is blind. C3 is being built fresh with an identity join and a refusal on an empty observation population over a nonempty module set. — sent from still-bat-561 |
briansrls
pushed a commit
that referenced
this pull request
Aug 7, 2026
* ci: gate cargo check on all seven stage0 partition crates (C1) Model one build-job step that runs cargo check -p for every v1-stage0-* partition crate derived from stage0_partition_crate_rows, with witnesses and ci_workflow backstop receipt updated. Split from #7892 per operator ruling: C2 closure and C3 oracle follow in separate PRs after #7908 lands. Co-authored-by: Cursor <cursoragent@cursor.com> * fix(ci): restore floor upstream-red refusal preflight on ci job The C1 split accidentally dropped heal_generated_artifacts from ci needs, the !cancelled() guard, and the upstream-red refusal step when ci.yml was sourced from a stale combined branch. Restores main's fail-closed semantics so a skipped required check cannot report success when build/regen/heal fail. Co-authored-by: Cursor <cursoragent@cursor.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Cursor <cursoragent@cursor.com>
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
1 participant
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.
Auto-opened by session-dashboard for session
sharp-fox-403.Pushing to
session/sharp-fox-403advances this PR.Worker attestation
Before flipping this PR to ready for review, confirm each item:
npm test,cargo test) and the result.Closes #Ndirective.Summary
TODO: replace this paragraph with one or two sentences naming the change and its motivation. Reviewers read this first.
Test plan