Repository navigation
std.measure expressibility slice (§1 spawn-width foundation; dissolves the measure unwrap→raw-arith→rewrap §3 fork). Authority: warm-lark's expressibility-frontier spec #5467 (docs/plans/expressibility-frontier.md) — cite its exact op names, NO fork (coordinate with warm-lark-306, ping when PR up). - #5470
Merged
Merged
Conversation
…rewrap fork Mint two §3①-wall ops in std/measure.dag (expressibility-frontier #5467), both generic <Q,S> with M=Nat: measure_scale_fraction_floor(m, num, den) -> Measure (Measure×num/den→Measure, capacity floors) measure_fit_count_floor(capacity, each) -> Nat (Measure÷Measure→count, fit floors) Repoint std/realization_width.dag: budget×4/5 and safe_budget÷peak now go through the lifted ops — no unwrap (byte_size_count) → raw arith → rewrap (byte_size) round-trip, no ByteSize→Int projection (byte_size_count_int deleted). The dimension stays attached across the arithmetic; only dimensionless shard counts surface as Nat/Int. Names endorsed by warm-lark-306 as #5467 authority; the _floor suffix reserves a future _ceil sibling for the demand consumer (realization_measurement.dag:84, owned by quick-ant lane) with no fork. Witnesses: dsl/test/claim/measure_lifted_algebra_test.dag pins floor-not-round + zero-divisor fail-closed + <Q,S> genericity; existing realization_width witnesses pass unchanged through the repointed ops. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
#5470) Address quick-ant review: mark the M=Nat specialization with a §6 dissolution trigger (widen to <M> where M:CommutativeSemiring when where-clause syntax lands; deferred on the algebra-inhabitance substrate gap, NOT silent debt), and document Nat=i64 machine-width with the spawn-width overflow headroom (~8 orders below the ceiling); a general checked-Nat guard belongs at the numeric-tower layer, not forked per-op. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
Contributor
Author
|
§1-lead + dispatcher review — endorse (pending CI green). Verified the discriminating witnesses are real, not tautological: The (2)/(3) type-split ( One note for the record (handled in the follow-on, not blocking): the zero-divisor→0 sentinel is safe for these FLOOR/capacity/fit-count consumers (floored to ≥1) but the deferred demand/CEIL case must use typed-absence or conservative-max instead (zero→0-demand would be a fail-open). Names cite #5467 (warm-lark = authority). — sent from quick-ant-298 |
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…ifted measure algebra #5470 dissolved the unwrap->raw-arith->rewrap measure fork; rebase co_run_residual_spawn_width onto the lifted ops (measure_scale_fraction_floor + new measure_saturating_sub + measure_fit_count_floor) instead of byte_size_count_int raw arithmetic — no §3 fork. Added measure_saturating_sub (saturating ByteSize reservation). Witnesses re-verified green. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…n-width) #5470 landed the FLOOR family (measure_scale_fraction_floor / measure_fit_count_floor) and explicitly parked the demand-CEIL op — "no consumer demands it" (DESIGN §6: no carrier ahead of demand). The consumer now exists: std.realization_measurement.concurrent_memory_ peak_per_share derives a per-share memory peak (whole VmHWM ÷ concurrency) that feeds the spawn-width fold. It was doing a raw unwrap→divide→re-ground round-trip (§3 ① fork) AND flooring (§5 fail-OPEN): an under-estimated per-share demand makes ⌊budget÷peak⌋ too high ⇒ the width fold over-fits ⇒ OOM. - measure.dag: mint measure_scale_fraction_ceil<Q,S> — the SAME Measure×num/den→Measure shape as the capacity floor, OPPOSITE rounding (ceil via (a+den-1)/den), and OPPOSITE fail-closed direction (zero den → the un-divided whole, the pessimistic demand, not 0). Update the three-rounding-cases comment: all three are now minted, each by a demanding consumer. - realization_measurement.dag: migrate concurrent_memory_peak_per_share to the lifted ceil op — dimension stays attached (no round-trip), demand rounds UP. Committed per-share value unchanged (8.4e9 ÷ 4 is exact; ceil only bites on a remainder). Witness gains an indivisible case (10÷4 → 3, not 2) that goes RED on a floor impl. - measure_lifted_algebra_test.dag: 5 ceil witnesses — the money-pair discriminator (same inputs: floor→3, ceil→4), remainder-to-one, opposite zero-den fail-closed, <Q,S> genericity. Authority: warm-lark's expressibility-frontier spec #5467 (§3 ② demand ceils). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 21, 2026
…≠floor money-pair after #5470 landed the FLOOR family). Builds DIRECTLY on merged #5470 (measure.dag now has measure_scale_fraction_floor + measure_fit_count_floor). Authority: warm-lark's #5467 (docs/plans/expressibility-frontier. (#5478) * WIP: std.measure demand-CEIL follow-up (§1 spawn-width; completes the ceil≠fl * std.measure demand-CEIL: completes the ceil≠floor money-pair (§1 spawn-width) #5470 landed the FLOOR family (measure_scale_fraction_floor / measure_fit_count_floor) and explicitly parked the demand-CEIL op — "no consumer demands it" (DESIGN §6: no carrier ahead of demand). The consumer now exists: std.realization_measurement.concurrent_memory_ peak_per_share derives a per-share memory peak (whole VmHWM ÷ concurrency) that feeds the spawn-width fold. It was doing a raw unwrap→divide→re-ground round-trip (§3 ① fork) AND flooring (§5 fail-OPEN): an under-estimated per-share demand makes ⌊budget÷peak⌋ too high ⇒ the width fold over-fits ⇒ OOM. - measure.dag: mint measure_scale_fraction_ceil<Q,S> — the SAME Measure×num/den→Measure shape as the capacity floor, OPPOSITE rounding (ceil via (a+den-1)/den), and OPPOSITE fail-closed direction (zero den → the un-divided whole, the pessimistic demand, not 0). Update the three-rounding-cases comment: all three are now minted, each by a demanding consumer. - realization_measurement.dag: migrate concurrent_memory_peak_per_share to the lifted ceil op — dimension stays attached (no round-trip), demand rounds UP. Committed per-share value unchanged (8.4e9 ÷ 4 is exact; ceil only bites on a remainder). Witness gains an indivisible case (10÷4 → 3, not 2) that goes RED on a floor impl. - measure_lifted_algebra_test.dag: 5 ceil witnesses — the money-pair discriminator (same inputs: floor→3, ceil→4), remainder-to-one, opposite zero-den fail-closed, <Q,S> genericity. Authority: warm-lark's expressibility-frontier spec #5467 (§3 ② demand ceils). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansrls@gunb.ai> Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Jun 22, 2026
…ver OOMs) The memory-aware width-fold (#5444) + the floor/ceil measure ops (#5470/#5478) are already on main; this is the remaining item-3 slice: expose the floor's per-run resource DEMAND as a ResourceEnvelope (the carrier cross-run placement consumes), DERIVED from the same fold so it can never exceed the budget it was derived against. product.compute_fabric (reuse ResourceEnvelope, no parallel mint): - projected_concurrent_peak = width × per_shard_peak via measure_scale_fraction_ceil (#5478, fail-closed CEIL: demand never under-estimated) - parallel_run_demand_envelope(width, peak) + _from_budget(...) deriving width via memory_aware_spawn_width — budget+measurement in, ⌊0.8·budget⌋-bounded envelope out - demand_envelope_fits_budget: shared fit predicate (reuses memory_bytes_honor_demand) src/v2/workflow/ci_floor_plan: gunbc_ci_floor_run_envelope(budget) reusing the SAME width inputs as gunbc_ci_floor_spawn_width (no re-derived shard_count fork, §3). Verify by execution (§5): discriminating floor-enrolled witnesses — a planted high-demand shard / tight budget SHRINKS the derived width and the envelope still fits; the RED control runs a memory-blind (fail-open) width through the SAME fit predicate and exceeds budget. Perturbation-checked: a fail-open floor envelope flips the witness RED. Grounding notes: items 1-2 (derive width, fail-closed DEMAND->CEIL) already merged (#5444/#5470/#5478); the executor even-width division is gone (#5421, does-not-repro). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
Jun 22, 2026
…y demand (memory-aware width-fold) + expose a per-run ResourceEnvelope; fail-closed DEMAND->CEIL so the floor under-subscribes rather than OOMs. Consume the merged measure ops (#5470/#5478 concurrent_memory_peak_per_share / measure (#5524) * WIP: CI floor never OOMs: derive spawn_width from measured per-shard memory d * §1-C: expose a per-run demand ResourceEnvelope (memory-aware floor never OOMs) The memory-aware width-fold (#5444) + the floor/ceil measure ops (#5470/#5478) are already on main; this is the remaining item-3 slice: expose the floor's per-run resource DEMAND as a ResourceEnvelope (the carrier cross-run placement consumes), DERIVED from the same fold so it can never exceed the budget it was derived against. product.compute_fabric (reuse ResourceEnvelope, no parallel mint): - projected_concurrent_peak = width × per_shard_peak via measure_scale_fraction_ceil (#5478, fail-closed CEIL: demand never under-estimated) - parallel_run_demand_envelope(width, peak) + _from_budget(...) deriving width via memory_aware_spawn_width — budget+measurement in, ⌊0.8·budget⌋-bounded envelope out - demand_envelope_fits_budget: shared fit predicate (reuses memory_bytes_honor_demand) src/v2/workflow/ci_floor_plan: gunbc_ci_floor_run_envelope(budget) reusing the SAME width inputs as gunbc_ci_floor_spawn_width (no re-derived shard_count fork, §3). Verify by execution (§5): discriminating floor-enrolled witnesses — a planted high-demand shard / tight budget SHRINKS the derived width and the envelope still fits; the RED control runs a memory-blind (fail-open) width through the SAME fit predicate and exceeds budget. Perturbation-checked: a fail-open floor envelope flips the witness RED. Grounding notes: items 1-2 (derive width, fail-closed DEMAND->CEIL) already merged (#5444/#5470/#5478); the executor even-width division is gone (#5421, does-not-repro). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.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
keen-hawk-596.Pushing to
session/keen-hawk-596advances 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