Repository navigation
FABRIC-MEM-GRANT-0: one memory grant carrier, one microVM sizing policy, one grain-parameterised rounder (reconciles #11883 + #11885) - #11992
Merged
Conversation
…grant carrier + microVM policy + one grain-parameterised rounder Parked record, not a PR. Program is parked on operator instruction; this commit exists so the work is durable. A second independent implementation is bright-ram-63 125659f. - product.fabric.memory_grant: sole_constructor MemoryGrant<P, A>, authority as a type parameter; provenance holds requirement or permit so an unstated axis without a permit is unwritable; two laws (below stated minimum, above ceiling), neither clamps. - gunbc.fabric_memory_grant_policy: fieldless sole_constructor MicroVmMemoryGrantAuthority token (DataRevealKey precedent) so the policy is the sole producer by construction; the ceiling is a PARAMETER of the fleet binding (no forked remainder subtraction, no invented fleet row); representability is bounded against int_inclusive_max FIRST and the ceiling SECOND, and the annotation says why the order is load-bearing. - std.measure round_up_to_grain: the corpus's one rounder, grain a declared FiniteByteSize input, subtraction form (pad first, one comparison, no checked_add). gunbc.floor_demand round_up_to_gibibyte_grain is now its gibibyte binding; GrainRounding moved to std.measure and three consumer import lines re-pointed (runner_microvm, floor/runner witnesses). Evidence (local claim_batch on the shared /cargo-target binary; these witnesses are NOT on the required gate): test.claim.fabric_memory_grant_witness_test 14/14 PASS, test.claim.measure_grain_rounding_witness_test 4/4 PASS (3 at first run; the fourth is the power-of-two control added after the finding below), the four re-pointed floor_demand / runner_microvm rounder claims PASS. Mutation controls: ceiling checked ahead of the sizing -> a_minimum_within_one_byte_of_the_bound_refuses_as_unrepresentable FAILs; checked-add restored in the rounder -> an_aligned_count_at_the_bound_is_its_own_ceiling (grain 1000) FAILs. Finding: at any power-of-two grain the checked-add and subtraction rounders refuse the SAME set (2^63 is a multiple of the grain), so a gibibyte-grain control cannot discriminate them; the discriminator uses grain 1000. bright-tern-814's annotation claiming otherwise was wrong. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…cy, one grain-parameterised rounder (reconciles #11883 and #11885) Base: session/royal-moth-544 @ 80ec506. Ported from session/bright-ram-63 @ 125659f: every fleet quantity the policy needs arrives as a parameter (no import of gunbc.runner_microvm, so the wiring item closes no cycle), the fleet binding is total, and the unstated-axis-through-the-real-route claim. Applied once: the compatibility default is a ByteSize derived from the gibibyte (review 69467, review 69468). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…rting it Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
…9638, DESIGN 3c) Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Contributor
Author
|
review 69638 addressed in d08c9b8: |
This was referenced Sep 22, 2026
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 22, 2026
Mirror-only, from the merged base. Fixed point proven by a second regen round with a binary verified to carry the rework: round two reports drift in std_measure.rs alone, so v1_compiler_emit_rust.rs is what the reworked emitter itself emits. std_measure.rs is excluded as before -- it is #11992's unmirrored grain-rounder, and #12027 is the PR that repairs it. EVIDENCE RE-ESTABLISHED AFTER THE REWORK, because the coproduct change touched emit_native_freemonoid_match and every earlier behavioural claim described a superseded revision: list_init identical three-arm chain, __fm.len() == 1 preserved refusals in closure 0, unchanged __fm.len() conditions 13 (2 exact, 11 floor), unchanged probe 5/5, exit 0 red control 3/5 FAIL, exit 1 So the rework is a pure refactor of how the refusal is carried, measured rather than asserted. The four enrolled witness rows all return true: nested_field_arm_and_its_successor_both_reach_the_emitted_chain, the_ordinary_two_arm_shape_still_lowers_natively, a_refutable_head_sub_pattern_refuses_rather_than_becoming_a_wildcard, a_guarded_arm_refuses_rather_than_running_unguarded. INSTRUMENT PROVENANCE, recorded because it nearly produced a false finding against this change. /cargo-target is shared across worktrees and sessions. A neighbouring session's build of v1-compiler overwrote the binary between the moment I verified it carried the rework and the moment I measured with it, so two witness rows reported false and a fixture emitted a textbook reproduction of the original bug -- from a compiler that predated the fix. Caught only because two greps of one file disagreed: the rework-only string counted 1 earlier and 0 later. Every measurement above was re-taken with a worktree-local CARGO_TARGET_DIR whose binary was verified by a string that exists only in the reworked code. The red control needs no such check: its artifact carries the two-way split and zero length-conditions, and witness row one establishes that the fixed emitter emits len() == 1 for that exact shape, so the output identifies its own producer. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 22, 2026
…r in agreement dag/gunbc/plans/dag_v2_defork_audit.dag is restored byte-for-byte to main. WHY, AND IT IS NOT THAT THE STALENESS WOULD GO UNCAUGHT. docs/plans/dag-v2-defork-audit.md is a registered PlanArtifact (via plan_registry_batch_b) regenerated ONLY by the whole-population claim_executor --required-regen. That round currently fails on 'generated surface drift: std_measure.rs' -- a real drift on main since #11992, already repaired in gunbc#12027 and not mine to re-fix. So editing this .dag meant committing a carrier whose mirror contradicts it. THE ARGUMENT I DID NOT GET TO MAKE, refused before I made it: "no CI job here runs the generated-artifact phase, so nothing gates it" is an argument that the lie would not be CAUGHT, not an argument that it is not a lie. A registered artifact whose mirror does not match its authority is a stale present-tense claim in a carrier a reader consults first -- the class gunbc.v2_compile_obligation_census filed itself. Ungated makes it worse, not admissible: an ungated artifact is one nobody will ever correct. NOTHING IS LOST. The substance the amendment carried already lives in gunbc.guarantee_stall.coercion_two_algebras_answer_one_question_stall, which states that the audit's coercion row rests on the two modules SHARING ZERO TYPE NAMES -- the right question for a resolver collision guard and the wrong one for a concept fork, since zero shared names is exactly what makes a fork invisible. The representation_boundary coercions row cites it too. The prose mirror was the carrier; the fact survives without it. AND THE MOVE NOT TAKEN: merging gunbc#12027's branch to unblock the regen locally. That converts an unrelated drift into a dependency between two lanes and inherits its refusals into this PR's evidence -- which is how a floor verdict was lost elsewhere today. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 22, 2026
… one missing declaration FOUR FAILING LANES, ONE DEFECT. The consumer half of the mirror carried the new diagnostic variant and the DECLARING half did not: compile_clean.rs referenced SiblingOperandEffectOrderUndetermined while v1_std_core.rs did not declare it, so the seed did not build -- compiler red, clippy cannot compile, floor cannot run the binary, witnesses is the aggregator echoing them. THE RULE THIS COST ME, WRITTEN DOWN: THE STAGE0 MIRROR IS TWO FILES FOR A NEW .dag VARIANT -- the enum's declaring mirror and every consuming mirror -- and the revert had taken v1_std_core.rs back to main state while compile_clean.rs kept my hand-authored arms. AND A SECOND ONE I CAUSED MYSELF: I PREDICTED THE INSTALL LIST INSTEAD OF TAKING THE REGEN'S. The regen named six drifted files; my script hardcoded four, and the one it missed was v1_compiler_infer_items.rs -- the mirror of the module where this change DECLARES item_is_effectful_callee. Install what the regen names, minus what other lanes own; never a predicted set. BOOTSTRAP ORDER, because the cycle is real: the hand-authored arms name a variant only the regen emits, so the seed cannot build to run the regen. Drop the arms, build, emit, install, restore the arms, rebuild. VERIFIED BY COUNT RATHER THAN BY A GREEN BUILD: src/v1/00_core.dag 4 src/v1/stage0/src/v1_std_core.rs 4 src/v1/stage0/src/cli_run/compile_clean.rs 4 and item_is_effectful_callee present in 04_items.dag, its mirror, and the consuming infer mirror. Generation 2 reports drift on std_measure.rs ALONE, so every mirror this change owns is at a fixed point; --required-regen-fixed-point answers fixed_point_equal=true. std_measure.rs is PRE-EXISTING drift on main since #11992, owned by #12027, and is deliberately not installed here. The peer resource wall is confirmed absent from the mirrors: the revert took fully. Co-Authored-By: Claude Opus 5 (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
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.
Summary
FABRIC-MEM-GRANT-0, reconciled from the two independent green implementations (#11883
session/bright-ram-63@ 125659f and #11885session/royal-moth-544@ 80ec506). One carrier, one policy, one rounder, one witness suite. Both superseded PRs are closed with a comment saying which base won.The defect this addresses is a bypass around the fabric transaction, not an absence of demand consumption: memory is screened before reservation and the runner reads the requirement, but memory is never converted into a grant, never atomically reserved against live host use, and never carried on
CellReservation. This PR lands the first of those — the grant carrier and the policy that mints one — and nothing else (see "What this does NOT do").Base chosen:
session/royal-moth-544, and whyBoth lanes converged on more than the brief recorded: both carry
MemoryGrant<P, A>with asole_constructorauthority token constructed only inside the policy's issue fold, and both take the per-cell ceiling as a parameter. Re-derived, the differences that decided the base:GrainRoundingandround_up_to_grain(bytes, grain)tostd.measure, reducesgunbc.floor_demand round_up_to_gibibyte_grainto its gibibyte binding, and re-points the three consumer imports (§3 replacement migration, cut at the root). bright-ram inlined a second grain-parameterised rounder in the policy beside floor_demand's — which is the fork.std.decl_ref DeclarationRef; bright-ram's areNonEmptyStr where brand(...)free text (§3: cite the symbol).MemoryCompatibilityPermit { default_grant, permitted_by, reason }rides inside the provenance, so "unstated axis without permit" has no constructor at the carrier and the policy refuses on its own typed arm. bright-ram carriedcompatibility_permit: Ref?beside a separatecompatibility_default: ByteSizeon the policy record — permit absent + default present is writable there, and the carrier needed a third refusal arm to validate it.Ported from
session/bright-ram-63gunbc.runner_microvmfor the cache allowance and admitted in its own frontier note that the wiring item (runner consuming the policy) would then close an import cycle. bright-ram's acyclicity argument is right: the binding now takes(allowance, ceiling), imports nothing from the runner, and is total (grain constructed viagibibyte_grain(), reference and permit are the module's own rows — noUnavailablearm left for a consumer to answer). The witness keeps the pairing obligation by executing the real allowance producergunbc_runner_microvm_guest_cache_allowance()and assembling the policy exactly as the wiring consumer will.the_fleet_policy_binding_grants_an_unstated_axis_under_its_own_permit).Not ported, with reason: bright-ram's token carrying
policy: Ref(the fixture policy can set that ref to anything, so it adds no guarantee over the type identity);microvm_memory_grant_is_compatibility_default(no consumer but its witness — §3c dangling; the carrier'smemory_grant_standing_is_requirement_checkedalready answers it).Applied once: the ByteSize repair (review 69467, review 69468)
gunbc_microvm_memory_compatibility_default_bytes: Int = 4294967296on both branches is nowdata gunbc_microvm_memory_compatibility_default: ByteSize = gibibyte_to_byte_size(g: gibibyte(count: 4))— the unit in the type, the magnitude reached throughstd.measure gibibyte_scale_factor_bytes, and the witness compares throughbyte_size_count.The four decided things, kept
int_inclusive_maxfirst (policymicrovm_memory_grant_size), the ceiling second (carrierissue_memory_grant). M1 shows exactly one claim goes red when the order is flipped.measure_grain_rounding_witness_test an_aligned_count_at_the_bound_is_its_own_ceiling). M2 re-measures it.a_minimum_within_one_byte_of_the_bound_refuses_as_unrepresentableuses a small ceiling and still expects the unrepresentable arm).MemoryGrantnames its Work and Attempt byFabricIdentity, carries no host, cell or ledger state, and is the value aCellReservationwill carry and one CAS will commit alongside occupancy.Topology precondition (a gate, not an item): exact per-Work sizing is valid only where Work is bound before the VM boots. Nothing here lets a guest discover its Work after boot.
What this carrier does NOT do
gunbc.runner_microvm runner_microvm_shape_after_cpu_admittedstill reads the requirement as a fit gate and sizes the guest from the cell remainder. The wiring item is a declared frontier (§3c) at the foot offabric_memory_grant_policy.dag, with the capability as its trigger: the microVM shape derives its guest memory from aMemoryGrant, with the remainder exposed as one nameable runner function and the runner's memory witnesses re-pointed at the granted size. Import direction for that wiring: runner → policy, never the reverse.CellReservation. Those are items 2+ of the program.required_gate_prefixeshas notest.claim.fabricrow, so this suite is discovered and declined by the required gate; a green check says nothing about these files. Evidence is the localclaim_batchrun below.Test plan — executed, at this head, with a binary built from it
Binary:
claim_batchbuilt locally (CTRL_BUILD_MODE=local cargo build --release --bin claim_batch, private target dir) from this branch's Rust tree, sha256ee16009ead17190ef367c71b826d6737b36a09ed94ce04642d5956d8ec6aa611. The change is.dag-only, so the Rust tree at every head below is identical to the one the binary was built from. Recipe per entry:claim_batch --source-root dag --source-root src/v2 --entry <entry> --functions <all test fns>. Every log line carries the binary path, its sha256,git rev-parse HEADand the dirty count.Green at
0bbf7a163f3(the semantic head;a65bcee222badds one//annotation block only, and the fabric suite was re-run there — see the last row):test.claim.fabric_memory_grant_witness_testtest.claim.measure_grain_rounding_witness_testtest.claim.floor_demand_witness_test— the two rounder consumers (gibibyte_grain_rounds_up_and_leaves_a_whole_gibibyte_alone,a_count_at_the_representable_bound_has_no_gibibyte_ceiling)test.claim.runner_microvm_witness_test—the_guest_cache_allowance_derives_from_the_receipts_last_unstalled_beat(the re-pointedGrainRoundedconsumer)test.claim.fabric_memory_grant_witness_testata65bcee222bMutation controls, each executed at
0bbf7a163f3(dirty=1) and the tree restored to dirty=0 before the next:policy.ceilinginstead ofint_inclusive_max(the ceiling-first order)the_policy_carries_the_ceiling_refusal_out_rather_than_resizing; both sizing claims stay green — which is why they are not coverage for this distinctionstd.measure round_up_to_grainrefusesn > max - (g-1)(the old checked-add pre-check restored)an_aligned_count_at_the_bound_is_its_own_ceiling(grain 1000) RED;a_gibibyte_aligned_count_at_the_bound_is_its_own_ceilingstays GREEN — the power-of-two control does not discriminate, as decidedMicroVmMemoryGrantAuthority { }appended to the witness modulefabric_memory_grant_witness_test.dag:416:3: error: sole_constructor type 'MicroVmMemoryGrantAuthority' cannot be constructed outside its defining modulea_grant_above_the_ceiling_refuses_and_does_not_clamp,a_demand_larger_than_the_cell_is_reported_against_the_ceiling,the_policy_carries_the_ceiling_refusal_out_rather_than_resizing,a_permit_default_above_the_ceiling_is_refused_by_the_ceiling_lawa_minimum_within_one_byte_of_the_bound_refuses_as_unrepresentableRED withruntime error [integer-overflow]: 9223372036854775807 + 1 does not fit in a 64-bit Int— the untyped abort the guard replacesa_demand_larger_than_the_cell_is_reported_against_the_ceilingREDNot run: the required floor. These modules are outside
required_gate_prefixes, so a green check on this PR is not evidence about them (and the floor's own SUCCESS-over-refusal defect is open — docs/plans/microvm-and-floor-wind-down-state.md §1).Superseded
session/bright-ram-63) — closed, comment says why.session/royal-moth-544) — closed, comment says why; this PR's base.🤖 Generated with Claude Code