Repository navigation
Bind two zero-arg stage0 partition helpers as data so each pure value evaluates once - #10530
Merged
Merged
Conversation
…n to data The stage0 partition DAG (stage0_module_dag), its resolve+fold receipt (stage0_partition_receipt_outcome), and the intermediate fold outcome are frame-invariant computations: their inputs are all pure data or constant-function return values, and no claim perturbs them. Previously, every claim that called stage0_partition_receipt_outcome() re-evaluated the entire module list concatenation, the cross-unit edge table, and the partition fold. The test module has 4 claims that consume this value directly (witness_runtime_unit_members_holds, witness_v1_infer_unit_members_holds, witness_v1_artifact_unit_members_holds, witness_partition_perturbation_member_coverage_holds) and 2 more that call it indirectly through stage0_partition_fold_ok and stage0_partition_r4_valid. The witness_perturbation test (ForwardSameInSameOut) only checks the determinism of the member-coverage comparison; it does not perturb the stage0 data. DESIGN.md section 2: a cache may discharge unavoidable recurrence but may never excuse authored duplication. This is a modelling fix (case c), not a cache — the partition derivation is frame-invariant and should be declared as data, not recomputed per claim. Changed: - stage0_module_dag: fn -> data - stage0_partition_receipt_outcome: fn -> data - stage0_partition_r4_valid: reads receipt data, skips partition_fold - stage0_partition_fold_ok: reads receipt data - stage0_single_crate_fold_outcome: reads dag data - All call sites: () removed from data references
briansrls
marked this pull request as ready for review
September 5, 2026 08:42
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: 3e15748e29
ℹ️ 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".
| ResolvePartitionRefused { cause: cause } => | ||
| Stage0PartitionReceiptResolveRefused { cause: cause } | ||
| } | ||
| data stage0_partition_receipt_outcome: Stage0PartitionReceiptOutcome = match resolve_partition_outcome( |
There was a problem hiding this comment.
When the required witness floor executes these consumers, it creates a fresh evaluation frame—and therefore a fresh data_cache—for every claim (required_floor_runner.rs:6088-6092, v1_interpreter.rs:5841-5846). Consequently this initializer still performs the resolve/fold separately for each of the five direct or indirect consuming claims, but changing the nullary producer from fn to data also removes that aggregate producer from the function-call recomputation census used to identify and enroll floor_pure_producer_share candidates. Thus the lift neither provides the claimed cross-claim reuse nor leaves the best sharing point observable; keep this as an enrollable nullary function or introduce genuinely run-scoped storage for the data value.
Useful? React with 👍 / 👎.
gunbai-bot
Bot
changed the title
Contributor
|
HOLD — do not merge. I asked for this to be landed earlier today; I am withdrawing that request. A full-artifact reconciliation I should have run first shows this PR activates a suppressed claim. Baseline main run 33954515928 → this PR's run 33954161068, every identity compared: That identity is enrolled in the cost-debt roster (
The The two What is needed: merge The general trap, now seen three times in this wave (#10538, #10542, here): editing the body of a claim that is enrolled in a suppression roster un-suppresses it, and it then executes with whatever the roster was suppressing — excess cost here and in #10538, a route gap in #10542. There are 605 identities across The check that finds it costs one artifact diff: sum the per-claim deltas, compare against the corpus total, and list added and dropped identities. Approvals do not catch this — three passed #10538, and one passed this. — sent from deep-wolf-853 |
This was referenced Sep 5, 2026
…s change collapses Review 61406 caught an authored duplication left standing by the previous commit. stage0_partition_r4_valid called resolve_partition_outcome a second time to pull the assignment, while matching a receipt whose own definition already embedded that same call -- two demands for one pure fact with a shared-state least common ancestor, which DESIGN section 2 names as authored duplication rather than a caching opportunity. It is the same defect this change exists to remove, one declaration away from the fix. So the resolve becomes its own binding, stage0_resolve_partition_outcome, and both the receipt and r4_valid read it. resolve_partition_outcome now has exactly one call site. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014qYnzwGtbQqwa7o6wcSoaX
Contributor
|
Green and reconciled at Reconciliation vs main
|
gunbai-bot Bot
pushed a commit
that referenced
this pull request
Sep 6, 2026
… evaluates once (#10530) * rust_crate_partition_witness: lift stage0 partition derivation from fn to data The stage0 partition DAG (stage0_module_dag), its resolve+fold receipt (stage0_partition_receipt_outcome), and the intermediate fold outcome are frame-invariant computations: their inputs are all pure data or constant-function return values, and no claim perturbs them. Previously, every claim that called stage0_partition_receipt_outcome() re-evaluated the entire module list concatenation, the cross-unit edge table, and the partition fold. The test module has 4 claims that consume this value directly (witness_runtime_unit_members_holds, witness_v1_infer_unit_members_holds, witness_v1_artifact_unit_members_holds, witness_partition_perturbation_member_coverage_holds) and 2 more that call it indirectly through stage0_partition_fold_ok and stage0_partition_r4_valid. The witness_perturbation test (ForwardSameInSameOut) only checks the determinism of the member-coverage comparison; it does not perturb the stage0 data. DESIGN.md section 2: a cache may discharge unavoidable recurrence but may never excuse authored duplication. This is a modelling fix (case c), not a cache — the partition derivation is frame-invariant and should be declared as data, not recomputed per claim. Changed: - stage0_module_dag: fn -> data - stage0_partition_receipt_outcome: fn -> data - stage0_partition_r4_valid: reads receipt data, skips partition_fold - stage0_partition_fold_ok: reads receipt data - stage0_single_crate_fold_outcome: reads dag data - All call sites: () removed from data references * Bind the resolve outcome too: r4_valid was recomputing the demand this change collapses Review 61406 caught an authored duplication left standing by the previous commit. stage0_partition_r4_valid called resolve_partition_outcome a second time to pull the assignment, while matching a receipt whose own definition already embedded that same call -- two demands for one pure fact with a shared-state least common ancestor, which DESIGN section 2 names as authored duplication rather than a caching opportunity. It is the same defect this change exists to remove, one declaration away from the fix. So the resolve becomes its own binding, stage0_resolve_partition_outcome, and both the receipt and r4_valid read it. resolve_partition_outcome now has exactly one call site. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_014qYnzwGtbQqwa7o6wcSoaX --------- Co-authored-by: Brian Searls <briansearls1@gmail.com> Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
gunbai-bot Bot
added a commit
that referenced
this pull request
Sep 7, 2026
…LocalRepoWetLane
* Control (b) seed-unavailable behavioral receipt for dag/std/logic.dag
Route the seed-unavailable control (b) onto LocalRepoWetLane per operator
ruling (session bright-ram-778, msg msg_aee406be-d956-48c7-88a6-fed609d5fcc9):
- New transport module (tools.self_host_logic_seed_unavailable_transport):
emit dag/std/logic.dag with the real gunbc binary, compile the emitted
Rust WITHOUT the seed crate (zero-external-dependency crate, self-contained
pure std types), run the witness binary, verify expected constants.
The emitted code from dag/std/logic.dag is self-contained with no external
crate imports beyond std, so the cargo build requires no network access and
the seed crate is absent at link time -- seed linkage is structurally
impossible by construction (DESIGN section 7).
- New witness test (test.claim.self_host_logic_seed_unavailable_witness):
self_host_logic_seed_unavailable_receipt_holds -> Bool.
- Exclusion row in gunbc.ci_layer_roots.witness_exclusion_frontier:
classified as LocalRepoWetLane, excluded from hermetic discovery because
the transport operations have no mock_response.
- Schedule entry in v2.workflow.local_repo_wet_terminal.local_repo_wet_schedule:
enrolled for execution by the required floor's local-repo wet lane.
This control tests whether the emitted candidate depends on the seed crate.
If the emitted code fails to build or run without the seed, that failure IS
the finding -- it would mean the emitted code is not in fact self-contained,
a first-order fact about self-hosting.
This is NOT a substitute for control (a). Control (b) tests seed independence;
control (a) tests whether the comparison discriminates. Neither establishes
the other, and a green (b) does not cover a missing (a).
* Correct control (b): use standard emitted-crate deps but exclude v1-compiler seed; document embedded-source boundary
The parent (bright-ram-778) identified that emit_v2_rt_module unconditionally
emits src/v1_rt.rs into every emitted Rust crate. This file is the v2 runtime
shim -- seed-derived source embedded in the emitted source tree (fourth
seed-dependency mode not denied by crate-absence controls).
Corrections:
- Use standard emitted-crate dependencies (im, serde, stacker, clap, etc.)
which v1_rt.rs requires for its runtime primitives
- Deliberately exclude v1-compiler (the seed crate) -- this is what control (b)
actually tests: the emitted logic builds and runs without the seed library
- Document the boundary: v1_rt.rs IS present (unconditional emitter behavior)
but its functions are NOT CALLED by the emitted logic module (dag/std/logic.dag
is pure type declarations and function definitions, no v1_rt references)
- The control denies execution, linkage, and fallback modes; names embedded
source as the fourth mode with stated boundary
- Update exclusion reason and schedule comments to match
* Enforce v1_rt call-site check in control (b) transport
Per review (bright-ram-778): the embedded-source boundary for the
unconditionally-emitted v1_rt.rs must be ENFORCED BY EXECUTION rather
than narrated in prose. The transport now:
1. Reads the emitted subject module (src/std_logic.rs for dag/std/logic.dag)
2. Checks for v1_rt:: call sites via string_contains
3. Refuses if any are found (typed refusal: subject outside denial scope)
4. Only proceeds to cargo build + witness run if the check passes
The red IS authorable: point this transport at any module that uses
concat/trim/length/rc_empty_map and the v1_rt:: check fires.
Also removed all "dead code elimination" claims from comments per
instruction: the source is embedded either way, elimination is the
optimizer's choice not a structural guarantee.
* Route control (a) onto LocalRepoWetLane alongside control (b)
Rehome self_host_logic_behavioral_witness_test from FalsifierSelfHostWet (dead,
DeclaredCadenceUnrealized) to LocalRepoWetLane (live, same lane as control (b)).
Per operator ruling (bright-ram-778): a control that EXISTS and is PROVEN but
NEVER EXECUTES is the worst of the three states -- worse than absent, because
it gets cited as coverage while carrying no information. DESIGN is explicit that
a tier where the machinery exists but nothing gates on it is itself a lie.
Changes:
- ci_layer_roots.dag: change control (a) exclusion from FalsifierSelfHostWet
to LocalRepoWetLane, preserve the FalsifierSelfHostWet provenance in reason
- local_repo_wet_terminal.dag: add WetScheduledClaim for control (a)
- self_host_logic_behavioral_witness_test.dag: update documentation to reflect
new routing and the separation from control (b)
Both controls now route through the same LocalRepoWetLane lane. The emission
target (dag/std/logic.dag) is shared; each currently does its own emit step.
A future optimization could share the emit and diverge only at cargo build.
This completes the brief's requirement: TWO controls on the existing agreement
corpus, both routed through a live executor.
* Widen v1_rt call-site check to all emitted .rs files (excluding v1_rt.rs)
Replace single-file check (src/std_logic.rs only) with crate-wide check:
enumerate all .rs files via shell.Find.FilesByNameSorted, exclude v1_rt.rs
(which defines the runtime functions), and check every other file for
v1_rt:: call sites. A failed read or any matching file returns false
(fail-closed).
This makes the instrument's population equal to the claim's population:
the control asserts NO emitted file calls into the seed runtime, and the
check covers every emitted .rs file.
* Add fixture test for v1_rt:: call-site check logic
Hermetic fixture that proves the slbu_check_no_v1_rt_calls mechanism
discriminates, without requiring gunbc emit or cargo build:
- GREEN: clean file with no v1_rt:: reference passes
- RED: file containing v1_rt::lookup fails the check (discriminator)
- GREEN: v1_rt.rs file (excluded from check) with v1_rt:: content permitted
These operate on synthetic file contents via Filesystem.Write/Read and
string_contains -- testing the CHECK FUNCTION in isolation.
* Fix receipt defects and §4c annotations on controls (a)/(b)
- Remove unused slbu_scaffold_dissolution_trigger (review 61030 finding 1)
- Delete the unreferenced DissolutionCondition data row and its import
- Fix vacuity in slbu_check_no_v1_rt_calls:
- Check found.success and refuse on failed file enumeration
- Refuse on empty file list (list_length > 0 guard) — no subject to check
- Fix exact-path exclusion: use ends_with(..., '/v1_rt.rs') instead of
string_contains substring match (was matching foo_v1_rt.rs etc.)
- Fix ordering: move scan to AFTER Cargo.toml and main.rs writes, so
what it scans is what cargo builds, not an intermediate tree
- Fix acceptance sentence: remove 'CONSTRUCTION OVER PROSE' and
'ENFORCES by execution' claims — a spelling search is a per-subject
validator, not a construction wall, and cannot carry an enforcement
claim. State what it actually does.
- Hoist 12 §4c grain violations from inline comments between
WetScheduledClaim elements in local_repo_wet_schedule() to a single
standalone // block above the function, joined by symbol identity
rather than adjacency
* Fix subject-presence check and answer ordering question
- Replace the non-emptiness guard with a genuine subject-presence check:
verify that a file ending with '/std_logic.rs' is in the enumeration
(the expected emitted module for dag/std/logic.dag). The name
'subject_present' now matches what the code does.
- Trim comment that claimed 'empty file list' was checked (it was, but
only as a proxy; the real check is now the specific module filename).
* Remove function-body // comments that caused 32 parse FAIL errors
The dag language only admits source annotations at module-item grain.
Comments (//) inside function bodies produce:
'source annotation sits inside a declaration body'
Removed 15 comment lines from self_host_logic_seed_unavailable_transport.dag
and 2 comment lines from the check_fixture_test.dag that were inside
function/test bodies. Essential rationale preserved as module-item
annotations above the function definitions.
* Fix ends_with call syntax: method call, not free function
ends_with is a String method in the dag language, invoked as
f.ends_with(suffix: '/std_logic.rs') not ends_with(s: f, suffix: ...).
The free-function form caused a runtime NoSuchFunction error on the
required-witnesses-floor run at 041a0c2.
No parse FAIL errors remain — confirmed 0 parse errors in the failed
run's logs. The only error was this runtime NoSuchFunction for ends_with.
* Replace ends_with with string_contains for path matching
ends_with is not available as either a free function or a method
on Primitive(String) in the dag runtime resolution context. The
free-function form produced NoSuchFunction, and the method-call
form produced 'no method surface on Primitive(T)'.
Use string_contains with path prefix + exact root match for the
v1_rt.rs exclusion (matching /v1_rt.rs or bare v1_rt.rs), and
string_contains for the subject presence check (std_logic.rs is a
unique enough filename in the emitted crate to avoid false positives).
* Fix cargo build failure: add missing text_lookup_work_counter feature
The emitted v1_rt.rs uses '#[cfg(feature = text_lookup_work_counter)]'.
Without declaring this feature in Cargo.toml, newer rustc emits
'unexpected cfg condition value' errors (under -D warnings configured
by the build environment). The behavioral transport (control a) already
has this fix; the seed-unavailable transport (control b) was missing it.
This caused the cargo build to fail with exit 101 on the floor run,
which was the actual failure behind observed=failed at 047cdae.
* Hoist two irrecoverable facts back as module-item annotations
Re-added two facts that were deleted with the function-body // cleanup
at 041a0c2, now at module-item grain where the grammar admits them:
1. Validator-not-wall claim (above slbu_cargo_toml, attached to the
call-site check): restores the third agreement site saying this is
a per-subject spelling search, not a construction wall. Three sites
now agree again (transport, witness test, ci_layer_roots).
2. Ordering rationale (above slbu_seed_unavailable_receipt): documents
that the scan must run after the writes because this substrate
evaluates let bindings in declaration order (eval_block, not data
dependency), so the ordering is carried by line position. A future
editor who moves the scan above the writes reintroduces the defect.
Also kept the 'NO seed crate dependency' note above slbu_cargo_toml
(the absence of v1-compiler is not visible from the code).
* Fix fixture test: route through real transport function, not a re-implementation
The fixture was re-implementing check_no_v1_rt_calls_in_file inline,
creating a parallel predicate that already diverged (no v1_rt.rs
exclusion). The third test (v1_rt_rs_with_calls_permitted) never
invoked any variant of the check, making it decorative.
Fixed: fixture now imports slbu_check_no_v1_rt_calls from the real
transport and calls it over a synthetic temp directory. Three tests
mirror the three behaviors: clean dir passes, v1_rt:: call in a
non-v1_rt file fails, and v1_rt.rs containing calls still passes
(the exclusion works). All three invoke the real function.
This resolves review 38602 findings 1 and 2.
* Thread writes_ok through slbu_check_no_v1_rt_calls for structural ordering
The ordering between the Cargo.toml/main.rs writes and the v1_rt:: call-site
scan is now enforced by DATA DEPENDENCY rather than by line position: the
scan accepts writes_ok (cargo_toml.success && main_rs.success) as a parameter,
so it cannot be evaluated until both writes have completed. Reordering the
scan above either write would reference an unbound variable — compile-time
refusal.
The ordering comment above fn slbu_seed_unavailable_receipt now names the
structural dependency rather than warning about line order.
Fixture test updated to pass writes_ok: true for all three cases (the
fixture tests the check logic in isolation; the write ordering is a
deployment guarantee tested by the wet lane).
* Honestly document containment-test approximation for unavailable suffix method
The v1_rt.rs exclusion and std_logic.rs subject check use string_contains
rather than ends_with, because ends_with is declared in std.primitives and
handled by the interpreter but not registered in the resolver's method
surface for Primitive(String) — a declared known gap at
v1_compiler_infer.rs:7428 (same class as starts_with on List receivers).
The annotation now says the check is a CONTAINMENT TEST standing in for
a suffix test, and names the gap that would let a tighter rung arrive.
* Fix false positive in v1_rt:: check: exclude use-import lines
The emitted std_logic.rs legitimately imports types from the v1_rt runtime
via 'use crate::v1_rt::{...}'. The previous check flagged ALL occurrences
of v1_rt:: in non-v1_rt files, including these use-import lines.
Changed to per-line check: a line containing v1_rt:: is a violation UNLESS
it is a use-import line (contains 'use crate::v1_rt'). This correctly
passes on the emitted subject module while still catching actual call-site
references like v1_rt::lookup(key).
Also fixed one remaining body-grain // comment in the fixture test that
was missed due to a brace-counting bug in the scanner script.
* Add 4b(3) rung drop row for spelling-search validator
The v1_rt:: call-site check in the seed-unavailable transport is a
per-subject spelling search (string_contains), not a construction wall.
This registers the honest rung: structurally-guaranteed -> mitigatable,
with the restoration trigger being the NEXT-RUNG TRIGGER already stated
in the transport header (emit runtime fragments from modeled source).
Also includes items (1) and (2) from e0b0c22 (fixture now imports
and calls the real transport function, third test invokes the real check)
and the per-line v1_rt:: check fix from 23bc824 (exclude use-import
lines to avoid false positives on legitimate runtime type imports).
* Clarify writes_ok as ordering device, fixture scope note
- writes_ok annotation now states it is an ORDERING DEVICE, not an error
signal; the write failure is separately typed as slb_stage_incomplete
through staged, so the conflation is unreachable on the real path.
- Fixture header notes it passes writes_ok: true and CANNOT detect an
ordering regression — that is deliberate, covered by the wet lane.
* Fix seed-linkage check: search for v1_compiler:: not v1_rt::
The check was looking for the wrong pattern. v1_rt:: appears in every
emitted module as legitimate same-crate runtime shim usage (e.g.,
'use crate::v1_rt::{VecCompat, VecJoin}'). This is infrastructure,
not seed linkage.
The actual seed crate prefix is v1_compiler:: — the same spelling the
behavioral transport uses for its seed leg, and the same crate that is
deliberately absent from Cargo.toml. The manifest half (no v1-compiler
dependency) is the stronger claim — structural rather than a spelling
grep — and the spelling check now searches for the correct namespace.
The per-line complexity (previously needed to exclude use-import lines
from v1_rt:: false positives) is no longer needed because v1_compiler::
has no false positives in emitted modules. The v1_rt.rs exclusion
remains for defense-in-depth (v1_rt.rs may reference v1_compiler in
comments about seed source files).
* Sequence temp-directory cleanup after all operations via dependency token
The cleanup Remove calls could race ahead of the scan, build, and witness
operations on a dataflow-ordered substrate. Fixed by threading a sequencing
token (seq) derived from the receipt verdict through the cleanup: seq is
computed as verdict || !verdict, and the cleanup calls consume seq as an
operand. On any scheduling substrate, cleanup cannot evaluate before
verdict because seq does not exist until verdict is available.
* Register spelling-search rung drop in the rung_drop roster
* chore: regenerate drifted generated artifacts (ci auto-heal)
Ledger-Repair-Judged: docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-rung-drops.md
Ledger-Rows-Repaired: docs/design-rung-drops.md self_host_spelling_search_check
* Replace spelling-search rung-drop with guarantee-stall row
The spelling-search check in the seed-unavailable transport was always a
VALIDATOR (per-subject spelling search for v1_compiler:: references), not
a construction wall. It never held the structural rung, so a RUNG DROP
with previous: StructurallyGuaranteed fabricated an event.
WHAT CHANGES:
- DELETE dag/gunbc/rung_drop/self_host_spelling_search_check.dag
- REMOVE SelfHostSpellingSearchCheck arm from LegacyProseIdentity
- REMOVE self_host_spelling_search_check from rung_drop roster
- CREATE dag/gunbc/guarantee_stall/self_host_spelling_search_stall.dag:
GuaranteeStall with current=Mitigatable, ceiling=StructurallyGuaranteed,
blocker=AwaitsOneGrounding, population=BoundedPopulation (2 members)
- ENROLL the new stall in guarantee_stall roster
- NARROW the transport header: the spelling search is a VALIDATOR, not a
construction wall; the structural half is the manifest (v1-compiler
absent from Cargo.toml)
The grep against the actual emitted output confirms zero false positives:
no emitted .rs file contains 'v1_compiler::'. The committed stage0 mirrors
(src/v1/stage0/src/) are a different population (19 hand-authored files)
and are not scanned by the transport.
Carrier: guarantee_stall (correct), not rung_drop (wrong).
* Replace tautology with standard cleanup pattern
The seq = verdict || !verdict tautology was a workaround for ordering
cleanup after verdict evaluation. Replace it with the standard pattern
used by emit_host_transport and other instruments: cleanups are let-bound
in declaration order after verdict, and their results are ANDed into the
receipt expression. This eliminates the constant-folding risk (cleanups
always evaluate because they feed the return value) and the unused-binding
risk (cleanup results are consumed by the && chain).
Also narrow the transport header: the spelling search is a VALIDATOR
not a construction wall; the structural half is the manifest
(v1-compiler absent from Cargo.toml).
Grep against actual emitted output confirms: 0 files contain
'v1_compiler::' (with colons). The committed stage0 mirrors are
a different population and are not scanned by the transport.
* Fix stale comment referencing removed seq tautology
* Add dissolution trigger for hand-authored Cargo.toml
Per review 61218 finding 2: the hand-authored Cargo.toml (literal TOML
concat) is a parallel authority that will drift from the emitter's
dependency list. Adds DISSOLVES WHEN comment tying it to the emitter
producing its own Cargo.toml from the modeled dependency declaration.
Review finding 1 (rung_drop carrier mismatch) is obsolete — the file
was deleted in 715061d, replaced by the guarantee_stall row.
Review finding 3 (string_contains validator pattern) is already
documented as a validator-not-construction wall and carried by the
guarantee_stall row.
* Rename slbu_check_no_v1_rt_calls to slbu_check_no_seed_crate_refs
Per review 61230 nit: the function was named for v1_rt:: but actually
checks for v1_compiler::. Renamed to describe what it does (check for
seed crate references) rather than an obsolete subject.
* Honest cleanup comment: name the lazy-evaluation leak
The previous comment claimed cleanup 'cannot silently leak temp directories'
but under a lazy evaluation model with short-circuit &&, a false verdict
never demands cleanup_out or cleanup_src, leaking the temp directories on
the failure path. The house pattern (every transport in this codebase)
relies on strict let evaluation to guarantee cleanup execution. Naming the
gap honestly rather than asserting a guarantee that depends on the
evaluation model.
* Add exemption note for hand-authored Rust driver source
Per review 61252 finding 2: slbu_driver_main_source is hand-authored Rust
(medium-as-string) without a dissolution trigger. Unlike the Cargo.toml
(which duplicates the emitter's dependency list), the driver source is
a subject-specific behavioral test harness. Exempt because there is no
emitter-produced test driver to drift from — no parallel authority exists.
* chore: regenerate drifted generated artifacts (ci auto-heal)
Ledger-Repair-Judged: docs/design-failure-modes.md
Ledger-Repair-Judged: docs/design-rung-drops.md
* Correct cleanup comment: measured facts, not lazy-evaluation caveat
snappy-crane-234 measured: let is eager (unreferenced bindings evaluate)
and && does not short-circuit (both operands always evaluate). Cleanup
always runs. But this is a property of the current interpreter realization,
not a declared substrate guarantee — if && ever gains short-circuit
semantics, cleanup silently stops without any test going red. Filed as
its own 4b subject by snappy-crane-234.
* Tighten cleanup annotation: cite probe names and existing failure-mode
Cite snappy-crane-234 probe names (let_is_eager_when_unused,
and_demands_right_even_when_left_false) rather than transcribing their
conclusion. Replace the speculative caveat about short-circuit semantics
with a one-line cite to the existing failure-mode row
realization_arms_diverge_on_whether_the_program_refuses.
* Fix parse errors: hoist function-body /// comment to module level
The cleanup annotation comment was placed between let-bindings inside the
function body, which the compiler treats as source annotations (module-item
grain only). Moved above the function and merged with the existing module-
level cleanup comment. Also updated to cite snappy-crane-234 probe names
and the existing failure-mode row
realization_arms_diverge_on_whether_the_program_refuses.
* Fix citations in cleanup annotation: probe names, not session id
Cite the probe names (let_is_eager_when_unused,
and_demands_right_even_when_left_false) directly rather than the session
that ran them. Session ids are transient and resolve to nothing. Also fix
the residual citation: the failure-mode row exists in another lane's branch
and may not land before this PR — state as pending rather than as a tree
fact.
* Fix cleanup annotation: drop && clause, cite gunbc#10647
The &&-does-not-short-circuit clause was my framing and did not survive
measurement. Under short-circuit && the cleanup still reaches the
filesystem because effects are let-bound (eager let). The property the
transport stands on is EAGER LET, one axis. Cite the pending PR
(gunbc#10647) for the residual (no declared property guarantees this).
* Add dissolution trigger for hand-authored Rust driver blob
Per review 61312 advisory: the Rust test driver had an exemption note
but no dissolution trigger. DESIGN requires a named trigger even when
the dissolving capability is not yet built. Adds DISSOLVES WHEN the
emitter produces a behavioral witness driver for a modeled subject.
* File guarantee_stall rows for hand-authored Cargo.toml and Rust driver
Both medium-as-string sites in the seed-unavailable transport now have
guarantee_stall rows (current=Mitigatable, ceiling=StructurallyGuaranteed,
blocker=AwaitsOneGrounding, population=BoundedPopulation), matching the
pattern already used for the spelling-search validator. Per DESIGN §4b
meta-obligation 2 ('no untracked stall'): each class below its ceiling
names its next-rung trigger via the roster, not only in prose.
* Fix witness_admission_test: rehomed behavioral witness is now on LocalRepoWetLane
The self_host_logic_behavioral_receipt_holds witness was rehomed from
FalsifierSelfHostWet to LocalRepoWetLane earlier in this PR. The test
that asserts its consumer cadence still expected FalsifierSelfHostWet,
causing Bool(false). Updated to expect LocalRepoWetLane.
* Enroll fixture test on wet lane, add exclusion
The three self_host_logic_seed_unavailable_check_fixture identities were
being discovered by the hermetic floor but have no mock for file operations
(shell.Mktemp.Dir, Filesystem.Write, shell.Remove.RecursiveForce). Route
to the wet lane alongside the main witness, and exclude from hermetic
discovery via the same reason string.
* Contract migration: rename witness_self_host_logic_falsifier_wet_consumer_holds
The test function name carried 'falsifier_wet' after the witness was
rehomed to LocalRepoWetLane — a meaning fork per DESIGN §3. Renamed
to witness_self_host_logic_local_repo_wet_consumer_holds. Added
annotation explaining the rehoming and citing the authority
(ci_layer_roots.dag exclusion row). Single occurrence in tree, rename
is free.
* Enroll seed-unavailable witness in floor_route_gap
The identity executes on the local-repo wet lane (WetScheduledClaim in
local_repo_wet_terminal.dag) and held in the most recent floor run.
This enrollment records only the hermetic unreachability — it is honest
because the identity HAS a real executing route. Follows the precedent
set by the sibling self_host_logic_behavioral_witness which is already
enrolled at line 328.
* Replace bare Cons enrolment with FloorRouteGapExpectation
Migrate from the bare Cons list entry (legacy form) to the
FloorRouteGapExpectation form, which pins the identity, operation
(Parents), and ground (NoMockResponse). Carry annotation stating
enrolment is not the route — the route is the WetScheduledClaim row,
and the identity was enrolled on the wet lane and held.
* Balance the braces that made the whole tree unparseable, so this branch can execute for the first time
Three required-lane runs on this branch failed at "module index refused: 2
unparseable .dag source(s)", which reports standing=measurement_unreached --
the instrument could not be BUILT, so no floor ran, no claims executed, and
heal failed for the same reason rather than for any generated-artifact drift.
Two defects, both purely syntactic:
local_repo_wet_terminal.dag a duplicated "expectation: ExpectedToHold {}"
and its closing brace, left over from an append
floor_route_gap.dag floor_route_gap_expectation_chunk_07 opened 7
braces (fn + 6 Cons) and closed 6
Verified no subject moved: 32 wet-scheduled identities before and after with
none lost, 101 FloorRouteGapExpectation rows unchanged, and every .dag file in
the diff now brace-balanced with depth returning to 0 and never going negative.
The parser's reported location is a character offset, not a line number.
Nothing semantic is touched. The behavioral-witness rehome, the chunk_07 rows
in located/expectation form, and the annotations are all as the lane authored
them, and none of them has executed even once.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
* Model JIT runner minting and join it to the owned-cell binding (#10661)
* Model JIT runner minting and join it to the owned-cell binding
generate-jitconfig is a different endpoint from the registration-token flow
already modeled as RegisterOrganizationRunner, and the difference is the reason
this fleet wants it: a registration token is a shared secret a machine uses to
register itself and then keep durable credentials on disk, while a JIT config is
minted by the caller for one runner identity and makes the runner ephemeral by
construction. It is not a different authority -- GitHub gates both on
organization self-hosted-runners write -- so the new effect arm answers with the
same permission rather than inventing a runner-lane permission beside it.
gunbc.runner_jit_mint joins the two facts that must hold before a credential
exists at all: the fabric cell must be owned, and the App credential must
actually hold that permission. Those are separate authorities, so this module
owns neither. Ownership is checked before the credential, and its witness uses a
fully sufficient credential so only the cell can produce the refusal.
Also retargets two attempt witnesses off bind_microvm_to_cell. Its argument is
sole_constructor, deliberately, so no test outside its module can build one;
exposing a builder would punch exactly the hole the seal exists to close, so the
refusal is exercised at the composable step the binder delegates to.
A 201 with an empty encoded_jit_config refuses rather than yielding an empty
credential -- status-only branching would boot a guest holding an empty drive
that waits out its whole deadline looking healthy.
Nothing calls plan_jit_mint yet; the lifecycle controller is its caller.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
* Witness that members_owned cannot currently refuse
The review accepted this PR's coverage narrowing partly on an annotation I wrote
claiming the ownership join is covered upstream where the snapshot is minted.
That was not true: members_owned had no witness anywhere in the corpus, and
FabricCellMember is an ordinary record, so the sole_constructor seal was never
the reason it went uncovered.
Checking it surfaced the larger fact. fabric_cell_member_ownership derives
ownership by building FabricCellSlotScope from the member's own slot, and
fabric_cell_subject_ownership answers Owned for every slot scope. A member
carries only a slot, so the Ensured arm is unreachable from a member and Absent
is never constructed -- members_owned returns true for every input, and its fold
seeds true so the empty cell reads as owned too.
That matters because a consumer reads it as a safety predicate: runner_jit_mint
refuses to mint a runner credential for a cell that is not owned. The refusal is
real in the arm receiving the Bool; the Bool reaching it cannot presently be
false. What actually rejects a malformed cell today is fabric_cell_shape's
Incomplete arm, which runs before ownership is consulted -- a different
authority than the one the refusal names.
These witnesses pin the current behavior rather than asserting a guarantee, so
the day ownership becomes variable they go RED and the consumer's refusal gets
re-examined instead of silently starting to fire.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01VQ1HbKBP5SH24N2zxExYmN
---------
Co-authored-by: Brian Searls <cutencool.work@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Bind two zero-arg stage0 partition helpers as data so each pure value evaluates once (#10530)
* rust_crate_partition_witness: lift stage0 partition derivation from fn to data
The stage0 partition DAG (stage0_module_dag), its resolve+fold receipt
(stage0_partition_receipt_outcome), and the intermediate fold outcome
are frame-invariant computations: their inputs are all pure data or
constant-function return values, and no claim perturbs them.
Previously, every claim that called stage0_partition_receipt_outcome()
re-evaluated the entire module list concatenation, the cross-unit edge
table, and the partition fold. The test module has 4 claims that consume
this value directly (witness_runtime_unit_members_holds,
witness_v1_infer_unit_members_holds, witness_v1_artifact_unit_members_holds,
witness_partition_perturbation_member_coverage_holds) and 2 more that
call it indirectly through stage0_partition_fold_ok and
stage0_partition_r4_valid.
The witness_perturbation test (ForwardSameInSameOut) only checks the
determinism of the member-coverage comparison; it does not perturb the
stage0 data.
DESIGN.md section 2: a cache may discharge unavoidable recurrence but
may never excuse authored duplication. This is a modelling fix (case c),
not a cache — the partition derivation is frame-invariant and should be
declared as data, not recomputed per claim.
Changed:
- stage0_module_dag: fn -> data
- stage0_partition_receipt_outcome: fn -> data
- stage0_partition_r4_valid: reads receipt data, skips partition_fold
- stage0_partition_fold_ok: reads receipt data
- stage0_single_crate_fold_outcome: reads dag data
- All call sites: () removed from data references
* Bind the resolve outcome too: r4_valid was recomputing the demand this change collapses
Review 61406 caught an authored duplication left standing by the previous commit.
stage0_partition_r4_valid called resolve_partition_outcome a second time to pull the
assignment, while matching a receipt whose own definition already embedded that same call --
two demands for one pure fact with a shared-state least common ancestor, which DESIGN
section 2 names as authored duplication rather than a caching opportunity.
It is the same defect this change exists to remove, one declaration away from the fix. So
the resolve becomes its own binding, stage0_resolve_partition_outcome, and both the receipt
and r4_valid read it. resolve_partition_outcome now has exactly one call site.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_014qYnzwGtbQqwa7o6wcSoaX
---------
Co-authored-by: Brian Searls <briansearls1@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Classify the 19 discarded shell-effect outcomes outside the printer scope (#10664)
* Classify the 19 discarded shell-effect outcomes outside the printer scope
16 of them are lawfully best-effort under one stated discriminator; 3 owe a
real distinction and sit in a subsystem with no producer and no consumer.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Record the entry-vs-module map: a cut here reds a witness and shrinks a monotone roster
"Dormant at both ends" overstated it. The two Bool entries have no callers; the
modules do not. merge_admission_fetch_stall_deadline_seconds is imported by
merge_admission_current_context and asserted by an enrolled witness, and
read_tested_subject / read_floor_receipt are enumerated sites of the
filesystem_io absence-establishment monotone roster, whose rows may leave by
deletion. A path-shaped grep and a module-shaped grep answer different questions
here; only the second finds importers.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Check all 16 against the mktemp-origin test by construction site, not by name
cache_dir is the member whose name asserts a lifetime its construction does not
have: both sites are shell.Mktemp.Dir(), so it is per-run and the discriminator
holds. Every other binding the sweeps reach is likewise a shell.Mktemp.* call
with no other origin and no shadowing. Recorded at the declaration, with the
naming defect named separately rather than fixed here.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* The population moved 19 -> 15: carry the ref the count was taken against
main deleted materialize_spark_serving_ollama_runtime_bundle with the whole
spark-serving archive-admission block while this was open, so four members left
by deletion of the subject rather than by being consumed -- package_delivery
11 -> 7, the other three modules unchanged at 5 / 2 / 1. The annotation citing
that function by name would have described nothing. Every count now names the
ref it was measured at, because a bare number cannot tell a real change from a
stale citation.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* State the selector and identify members by declaration and arm, not by count
Two honest measurements disagree by one: shell-only reads 14, shell-or-Filesystem
reads 15. The wider selector is the right one -- the defect is an ignored effect
outcome, not a property of which service produced it -- and it is now written
out rather than implied by a grep. Membership is rostered by module, enclosing
declaration and the arm each sweep follows, because provider_wire_evidence's
five members share one declaration and would collapse to one at declaration
grain. bmc_onboard write_netrc is named as deliberately out of population rather
than silently dropped: #10574 deletes it, so the original 19 was branch-relative.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Three sites, two defects, two modules: say which count is which
Two independent reviewers summarized the OutcomeSemanticallyRequired class as
"two" -- the count of defects and of modules, not of sites. A classification
whose thesis is that a count needs its selector, its ref and an identity roster
should not leave its own count ambiguous.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
* Name the instrument: drop the transcribed census totals from all four modules
DESIGN §6 -- a measurement is cited by naming the producer that re-derives it,
never by copying its numbers into prose. Adding a revision and a selector made
the totals attributable without making them re-derivable, and four modules each
holding a copy is four ledgers maintained by hand independently of their
subjects. The totals are gone; what remains is the SELECTOR (the instrument that
re-derives the population at any ref) and the members NAMED by module,
declaration and arm. The identity roster also carries what a total never could:
main's deletion of materialize_spark_serving_ollama_runtime_bundle retired its
members by deletion of the subject, which a count cannot distinguish from a
member being consumed.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01PGHDC1pbrgHLFj6BPfJNGA
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
* Review is a function: exclusive criteria mapped to calls, folded to one verdict and one piece of worker feedback (#10665)
* Review is a function: exclusive criteria mapped to calls, folded to one verdict and one piece of worker feedback
gunbc.roadmap.roadmap_review_function writes the review as review(subject) = aggregate(map(criteria,
criterion_review)): ReviewSubject is the one input every criterion sees, criterion_review builds a
criterion's whole call (its brief and verdict path), review_calls is the map over the roster, and
review_aggregate folds the evidence into the belt's reconciliation and the worker's feedback. The belt
now builds each reviewer's brief through criterion_review instead of hand-assembling it.
The criteria roster is proven an exclusive partition (review_criteria_are_exclusive_parts: distinct keys,
distinct grounding propositions) and gains extdeps-placement, grounded on s1.grounding-intersubjective:
does the change carry a fact other parties already agree on without pointing at the shared authority,
or put such a fact in the wrong layer (an upstream fact inside a product module, our policy or
observations inside extdeps, a hub enumerating products).
WorkerFeedback is the recomposition for the person who acts on it: findings regrouped by path in
criteria order, identical rows folded once, a path named by two criteria counted as the residual
(overlap_count), unjudged criteria listed as not reviewed. The reconciliation's failure detail is that
text, so the continuation turn and the board show the worker the same smoothed feedback.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* The review roster is derived from the design argument: each proposition carries its own review reading
gunbc.design_argument rows are now DesignRow { proposition, review? }: the proposition of the serial
argument plus, where it is checkable on one change, the reviewer's question and tells. The section
lists, design_propositions and design_argument are derived from the rows unchanged. gunbc.roadmap
.roadmap_review_criteria no longer authors a roster: review_criteria is flat_map over the rows with a
review reading, keyed by the proposition id minus its section prefix. Adding, changing or retiring a
criterion is one edit to the proposition's row and nothing else (operator: DESIGN criteria flow to
reviews with no dual representation). Witness keys follow the derivation (closed-grounded-substrate,
minimize-redundancy, grounding-intersubjective); the reviewer-spread witness reads the live keys.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* The belt realizes the review plan and judges through its fold: revision-bound calls, exact join, streaming feedback
Review 5125854144 on the first cut: the modeled map and fold sat beside production. Now they are it.
- ReviewPlan { revision, subject, calls }: the revision is the roster's content (any change to a criterion's
key, question or tells moves it); a call carries no verdict path (review_verdict_instruction is the
realization's, appended with the path it mints).
- ReviewObservation is bound to call id, subject id (node@head) and plan revision by the path the belt read it
from; review_join refuses unknown, duplicate, other-subject and other-revision observations by name and
keeps every planned call in the denominator (missing = awaiting). A subset of approvals is Pending, not
Complete.
- The belt builds the plan (belt_review_plan_for_head), realizes plan.calls with revision-keyed artifacts and
units (belt_review_call_key = <revision>-<criterion>), and publication and the workflow review segment
consume review_aggregate's report; belt_review_evidence, review_all_approved and the direct
review_reconcile calls are gone from production. Workflow evidence carries ReviewReport.
- Temporal rule: a head reviewed under an earlier roster is explicitly superseded -- old verdicts are not
this plan's observations, the restart is reported as ReviewPlanSuperseded with the stale count.
- review_criterion_identities_are_unique replaces the exclusivity claim; path grouping is presentation only.
- WorkerFeedback carries the incomplete calls; the text says the report is not complete and names them.
- DesignRow.review is PropositionReviewDisposition: ReviewableOnChange { parts } | NotReviewableOnChange { reason };
each part names its criterion key (extdeps-placement for s1.grounding-intersubjective).
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
* Operator entries for the review function: review one attempt's head on demand, and read its aggregate report
belt_review_head_for_instance is the one path a head is reviewed through -- the tick after verification
and the operator on demand (belt_review_head_cli) -- and belt_review_report_for_instance the one report
(belt_review_report_cli, JSON with state, detail, approved, incomplete, could_not_judge, overlap and the
worker feedback text). The operator entry does not verify and publishes nothing; publication still gates
on verification and the aggregate. review_report_json is the report's wire.
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_019iXPtAqzPaNBZbaaM5rxrY
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Claude Fable 5.1 <noreply@anthropic.com>
* Move the route-gap annotation to the grain §4c admits, and make it describe the six rows it actually covers
Four required-lane runs on this branch have now failed. The first three were an
unparseable tree; this one got past the module index and refused on the
annotation itself:
floor_route_gap.dag:863-865: source annotation sits inside a declaration body.
Only module-item grain is modeled; move it above the declaration it describes.
§4c admits only standalone leading // blocks attached to module-scope
declarations. A row inside a Cons chain in a function body is not a module item,
so a per-row annotation is inadmissible by construction. The content was right
and its placement was not; it moves into the existing block above
floor_route_gap_expectation_chunk_07, where the enrolment-is-not-the-route
sentence already lives.
The same block also asserted "these five route gaps ... all five executing and
holding on that lane" over a chunk that now carries six. That sentence was true
when written and is invalidated by the row added beside it, which is precisely
the failure mode §4c makes undetectable: no Accepted program reads an
annotation, so a stale one never reds and keeps reading plausibly. It now states
the six explicitly and separates their evidence -- the five eval_model probes
were observed by the run that produced their gaps; the sixth is enrolled beside
its own WetScheduledClaim row and is established by whichever run admits it --
and puts the maintenance obligation on whoever adds a seventh.
No row, identity, operation or ground changed: six FloorRouteGapExpectation rows
before and after, and the file's brace delta matches main's.
Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WgiDD3VoavwLrcu832nJ2V
* Fix annotation-position parse errors in floor_route_gap chunk_07
Move function-body // comments to module-item grain above the function
declaration. Same class of error as earlier in this PR: source annotations
inside a declaration body are refused (only module-item grain is modeled).
* Fix stall subject: v1_compiler:: not v1_rt::
The stall was created before the search pattern was changed from v1_rt::
to v1_compiler::. Subject string was stale — said v1_rt:: but the check
searches for v1_compiler::.
* fix: brace balance in floor_route_gap.dag (473/473); remove stale falsifier enrollment for behavioral receipt
floor_route_gap.dag:
- Added 3 fixture expectations (seed-unavailable check_fixture identities)
- Added corresponding Cons nesting closures (3 structural opens + 3 closes)
- Updated annotation: chunk carries NINE identities, run 34050705404
- Braces balanced: 473 opens, 473 closes (was 473/472, fixed +1 fn close)
wet_receipt_enrollment.dag:
- Removed self_host_logic_behavioral_receipt_holds from
falsifier_self_host_wet_template_entries (identity migrated to
local_repo_wet_terminal WetScheduledClaim, no longer enumerated in
falsifier roster; §3 smell resolved)
* Fix fixture vacuity: give v1_rt.rs actual v1_compiler:: reference; remove run number from annotation
The fixture directory_with_v1_rt_containing_calls_passes claimed it tested
that a v1_rt.rs with v1_compiler:: in comments passes the check, but the
file content had NO v1_compiler:: at all (unimplemented!() stub). Fix by
adding a prose comment referencing v1_compiler::lookup. The check still
passes because v1_rt.rs is excluded from the scan by name containment.
Also remove the transcribed run number 34050705404 / be79b78 from the
floor_route_gap annotation per section 6 (measurement artifacts do not
belong in authority files).
* Fix comment: local_repo_wet_terminal header says v1_compiler:: not v1_rt::
The schedule header for CONTROL (b) said 'The transport's v1_rt:: call-site
check' but the transport checks for v1_compiler:: (the seed crate namespace).
v1_rt is the runtime shim (emitted unconditionally); v1_compiler is the seed
crate that is deliberately absent. The comment misnames the checked token,
which is a meaning fork (DESIGN §3: one name, two materially different
meanings).
---------
Co-authored-by: gunbc-ci-auto-heal <gunbc-ci-auto-heal@users.noreply.github.com>
Co-authored-by: Brian Searls <cutencool.work@gmail.com>
Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
Co-authored-by: gunbai-bot[bot] <289086189+gunbai-bot[bot]@users.noreply.github.com>
Co-authored-by: Brian Searls <11205878+briansrls@users.noreply.github.com>
Co-authored-by: Brian Searls <briansearls1@gmail.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.
Summary
stage0_module_dagandstage0_partition_receipt_outcomewere declaredfnwith zeroarguments. A zero-arg
fnis a frame-invariant computation that pays its full cost onevery demand; the same value, bound as
data, evaluates once per module load. This PRchanges both declarations to
dataand updates every call site, including one inside theproduction file
src/v2/workflow/rust_crate_partition.dag.This is DESIGN.md §2 demand minimization applied at its cheapest point: the repetition here
is authored duplication with a shared-state least common ancestor, so the fix is to share
the first value, not to cache a later request.
Lane context:
v2.test.claim.rust_crate_partition_witnesscarries 637,556 eval_steps across4 claims over 100ms in the
required-floor-claim-costcensus.Why this shape and not a fixture shrink
Every other lane in this wave shrank a demanded test fixture. This module is different, and
the difference is load-bearing:
rust_crate_partition_witness_test.dagimports neither theemit nor the translate pipeline, so there is no heavyweight
TargetModelto replace. Thecost is repeated evaluation of a pure value, which is why the fix is a declaration change
rather than a fixture. (I had earlier asserted this whole family was emit-bound; that was
wrong, and this module is the counterexample that corrected it.)
Test plan
Measured, not asserted: the
required-floor-claim-costartifact from this PR's ownrequired-witnesses-floorrun, compared per-claim against the same artifact onmain.Ranked on
eval_steps, which is deterministic —observed_cpu_msswings ~38% run to runand is not a basis for a before/after claim.
Not built locally by design: the session container OOM-kills across the shared slice, so
verification is CI's.