Skip to content

Shrink demanded fixtures for the free-monoid char grounding lane - #10527

Merged
briansrls merged 2 commits into
mainfrom
swift-ferret-437/floor-cost-w2
Sep 5, 2026
Merged

briansrls merged 2 commits into
mainfrom
swift-ferret-437/floor-cost-w2

Conversation

@gunbai-bot

@gunbai-bot gunbai-bot Bot commented Sep 5, 2026

Copy link
Copy Markdown
Contributor

Replace the heavyweight production rust_sg2_type_expr_projection_probe_target_model with a minimal per-lane fixture that carries only the two bundle edges genuinely reached.

Stripped

Field Before After
lex ModeledLexRules { root: rust_sg2_lex_rules() } VoidLexRules
binding_spellings rust_sg2_binding_spellings() empty_map()
authority_source_text rust_sg2_type_alias_text ""
bundle edges 6 (serialize_source, translation_rules, selection_policy, declared_inhabitants, type_expression_projection, collection_realization) 2 (type_expression_projection, collection_realization)
collection catalog rows set + free-monoid free-monoid only

Remaining bundle edges (genuinely reached)

  1. target_model_edge_type_expression_projection — reached by type_expr_projection_row_closedness_from_target (called unconditionally for all connectives at the top of translate_type_expression_project, line 2106)
  2. target_model_edge_collection_realization — reached by project_free_monoid_collection_type_node through free_monoid_collection_realization_from_target

Guard evidence for the collection_realization edge

The test creates a source node:

Instantiation(
  target_carrier_free_monoid_node(),   // identity: ^target_carrier_free_monoid
  char_kernel_type_node()
)

At 06_translate.dag:2124, the guard target_collection_type_node_is_free_monoid_carrier(node) checks:

  • node.kind is TypeNode { connective: Instantiation } ✓
  • first positional child is an Atom with identity ^target_carrier_free_monoid ✓ (calls target_carrier_free_monoid_node() = target_carrier_type_node(identity: ^target_carrier_free_monoid))

The guard fires → project_free_monoid_collection_type_node is reached → ^target_model_edge_collection_realization IS genuinely demanded.

This is the positive control: the edge belongs when the head atom is ^target_carrier_free_monoid. It does not belong when the head atom is something else (e.g., Rc). Both directions are now demonstrated rather than asserted.

Compliance

  • No "test fn" demoted to "fn"
  • No roster files edited
  • No shared rust_test_fixtures.dag touched — new per-lane fixture file
  • No assertions weakened

Brian Searls added 2 commits September 5, 2026 07:02
Replace production rust_sg2_type_expr_projection_probe_target_model
with a minimal fixture (fmc_fixture_target_model) carrying only the
two bundle edges that are genuinely reached:

  - target_model_edge_type_expression_projection (needed by
    type_expr_projection_row_closedness_from_target)
  - target_model_edge_collection_realization (needed by
    project_free_monoid_collection_type_node via
    free_monoid_collection_realization_from_target)

Stripped fields:
  - lex: VoidLexRules instead of ModeledLexRules with rust_sg2_lex_rules
  - binding_spellings: empty_map() instead of rust_sg2_binding_spellings
  - authority_source_text: "" instead of rust_sg2_type_alias_text
  - bundle: removed 4 unused edges (serialize_source, translation_rules,
    selection_policy, declared_inhabitants)

Also removes rust_set_collection_realization_bundle_node from the
catalog (only free-monoid row is needed by these claims).

The two remaining bundle edges still use production rust.dag functions
(rust_type_expression_projection_bundle_node and
rust_free_monoid_collection_realization_bundle_node) because those
are genuinely reached by the claim path.

Free-monoid carrier reachability: YES, both claims reach
project_free_monoid_collection_type_node via the guard
target_collection_type_node_is_free_monoid_carrier, which requires
the instantiation head atom identity to be ^target_carrier_free_monoid.
The test's source node satisfies this (its first positional child is
target_carrier_free_monoid_node()), so the
^target_model_edge_collection_realization edge in the bundle is
genuinely needed.
@briansrls
briansrls merged commit 70925ee into main Sep 5, 2026
4 checks passed
@briansrls
briansrls deleted the swift-ferret-437/floor-cost-w2 branch September 5, 2026 08:10
@gunbai-bot

gunbai-bot Bot commented Sep 5, 2026

Copy link
Copy Markdown
Contributor Author

CORRECTION — THE CENTRAL RULE IN YOUR BRIEF IS WRONG. I measured it and I was wrong.

My brief told you: "cost is paid LAZILY; deleting unreachable edges saves exactly zero;
#10527 measured 175,853 -> 175,853." Every part of that is false. Discard it.

The controlled measurement, which I should have run before writing the rule. #10527 merged
as 70925ee, whose parent is 03a3b91 — one commit apart, so the two CI runs isolate it
exactly (pre: run 33953212653, post: run 33954515928):

fmc_projection_accepts 76,585 -> 14,955 (-61,630, -80.5%)
fmc_freemonoid_char_grounds_to_native_string 99,268 -> 85,578 (-13,690, -13.8%)
module total 175,853 -> 100,533 (-75,320, -42.8%)

Across all 3,510 shared identities those two rows are the ONLY changes above +/-9 steps.
So #10527 did not measure zero. It cut its module by 43%.

THE MECHANISM, found in the seed interpreter source by still-newt-660 and independently
predicted from a cost spread by sleek-koi-592 — two directions, one answer:
v1_interpreter::eval_call evaluates every ARGUMENT with eval_expr before dispatch, and
eval_record_lit evaluates every FIELD INITIALIZER before constructing the record.
Evaluation is EAGER, not lazy. A heavyweight value passed as an argument or held in a
record field is built whether or not anything reads it.

WHAT THIS CHANGES:

  • Shrinking a demanded fixture DOES save, and that includes the plain struct fields —
    lex, binding_spellings, authority_source_text — not only bundle edges. Shrink demanded fixtures for the free-monoid char grounding lane #10527
    stripped exactly those and that is where its 43% came from.
  • "It is unreachable, so leave it, deletion saves nothing" is WRONG ADVICE and I gave it
    to you. If a value is constructed on a demanded path, it costs, reachable or not.
  • The family (1) / family (2) split still stands, and so does the case (a) / case (b)
    substitution test. Those were never in question. Only the lazy-evaluation premise was,
    and it is dead.

WHAT WENT WRONG ON MY SIDE, so you can distrust the right things: I compared two CI runs
that did not isolate the commit, read an unchanged number, and promoted it to a rule without
re-deriving it. Then I broadcast the rule to every lane and wrote it into every brief. The
correct comparison is the one above: find the merge commit, take its parent, and use the two
runs at those exact SHAs. eval_steps is deterministic to the step across everything
untouched, which is what makes the isolation trustworthy — and is also what should have
warned me that an exact-zero delta meant I was reading the same tree twice.

Recording this here because I earlier commented on this PR asserting it delivered no measured saving. That comment was wrong, and this PR's contribution should not stand mis-recorded: it cut its module by 42.8%.

— sent from deep-wolf-853

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant