Repository navigation
Derived-node identity step 2: the generic-identity census (gunbc test //gunbc/instruments:generic-identity-census) - #13290
Conversation
…ment (output grain) v1.tests.claim.generic_identity_census reads the typed graph and records, per stored type node, which generic-identity marks it carries. Its blind spot is a typed UNOBSERVED population in every receipt. Not ready to push: the mirror and lib.rs line were emitted by a local compiler that is not main's emitter and must be regenerated; the gunbc test label and the callee-argument column are not written yet. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d-for-want-of-context
claim_executor --regen-round-cost in a standalone clone, looped to rebuild_packages=0. The census mirror and lib.rs line were already a fixed point. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
NO-LAND at this head. The output-grain census, typed UNOBSERVED rows, sorted receipt, label, and admitted host transport are a sound shape, but the reader currently turns absence of an observation into positive semantic answers.
-
gi_type_mentions_parameterrecognizes an owner's value-parameter mention only through theTypeParameterdeclaration mark. If that occurrence is itself one of the unmarked/lost carriers under measurement, it returns false;gi_foreign_readingthen recordsForeignParameterInNoValueArgument, which claims “unbound for want of context” even though the real answer is “the owner argument's identity was not observable.” Add an explicit indeterminate/unobserved arm (or another identity-backed observation) rather than treating no marked mention as proof that no value argument mentions the parameter. -
The fixture has the same absence-as-success problem.
bound_call_is_cleanis only the negation of a foreign row, so it holds if thecaller_functioncarrier disappears from the walk.collision_lost == falseis rendered assubstituted, although false also means the relevant carrier was not observed. Require a positive row for the call carrier and make the reading tri-state: left unsubstituted / positively observed substituted / unobserved. -
The module says it reads every kept signature parameter/return, but
gi_sig_rowsreturns[]for every signature with no declared type parameter. A nominally non-generic signature carrying a leaked foreign parameter is therefore silently omitted and is not one of the four UNOBSERVED populations. Either walk all signatures (ordinary concrete leaves are already filtered later) or declare that population explicitly.
These are measurement-validity blockers, not objections to using output grain. The current rows can support the present “left unsubstituted” observation, but the instrument cannot durably distinguish a repair from a lost/unwalked carrier until those absences have their own arm and positive controls.
1. gi_foreign_reading is three-valued. "No marked occurrence in the owner's value arguments" no longer reads as "no occurrence": a leaf spelled as the parameter and carrying no mark is ForeignParameterValueArgumentUndecided. 2. The bound-call control and the collision reading rest on ResultCarrierObservation, which says whether the carrier was seen at all. 3. gi_sig_rows reads every signature, not only those declaring a type parameter. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…cuted control owner_argument_arms_discriminate asks about one marked parameter under three supplied owners built from head_of's real signature and requires three different answers. missing_carriers_are_unobserved requires Unobserved for a name with no item and for an item with no body. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
LAND. The three measurement-validity blockers are closed at this head. Foreign-parameter cause is now positively discriminated: exact declaration-mark reachability wins, an unmarked same-spelling value-argument leaf is ForeignParameterValueArgumentUndecided, and InNoValueArgument is reached only after both are absent. Result-carrier standing is explicit rather than inferred from row absence: the clean control requires an observed Int carrier, the collision reading has observed-unsubstituted / observed-substituted / unobserved outcomes, and supplied-node controls execute both observation arms. gi_sig_rows now walks every signature, allowing a nominally non-generic signature carrying a foreign parameter to produce a row. The new three-arm owner control and missing-carrier control are discriminating, and the receipt remains sorted and byte-stable. No infer behavior is changed by this instrument.
…pt the branch's superset) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…tstrap to RestResult #13290 landed the IAM bootstrap in the old shape. Its fifteen IAM/IAM-admin/IAM-deny/secret-manager/ userinfo operations lose their outcome field; every .outcome-beside-body read becomes a match on RestAnswered/RestRefused with the same branches and texts. The policy readers split into an answered reading and iam_bootstrap_policy_refused; the policy writes return IamBootstrapPolicyWrite, whose refused arm keeps the raw RestRefusal for bootstrap_authority_publication_refused. The authority predicates take RestRefusal (they never decided on success). Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Step 2's first task in
docs/plans/derived-node-identity-design.md§7: make the measurement an instrument. Scheduled by gentle-dove-36; classgunbc.recurring_failure_modegeneric_identity_decided_by_spelling. No edit tov1.compiler.infer.What it is
v1.tests.claim.generic_identity_censusis a pure.dagreader overcompile_to_resolved→TypedModule.func_env+TypedModule.items, on the precedent ofv1.tests.claim.carrier_realization_census. For every type node the typed graph keeps, it records:Node.declarationTypeParametermark, theTypeVariablemark, both, or neither;foreign_in_a_value_argument, a substitution loss); no leaf carries the mark and none is spelled as the parameter (foreign_in_no_value_argument, unbound for want of an expected type); or a leaf is spelled as the parameter and carries no mark (foreign_value_argument_undecided, claimed as neither cause).Carriers read, for every signature whether or not it declares a type parameter: a signature's parameter and return types, the three type fields of each
ResolvedFormal, and the resolved type of every expression in a function body.Output grain, and its blind spot
The plan describes an event tap inside
unify_genericsandsubstitute_generics_apply. Those are pure folds with no output channel, and adding one would grow the frozen seed to take a measurement. This reads what those folds stored instead.What it cannot see is a typed population in every receipt, never a zero.
generic_identity_unobserveddeclares four: call-plan formals; the operands and maps of each unification; alias-chain and record-instantiation intermediates; signatures whose formals were never bound. Each row names what would observe it. The driver refuses a receipt that carries noUNOBSERVEDrow.The label
gunbc test //gunbc/instruments:generic-identity-census(GenericIdentityCensusProducer). Run by name, on no lane.fixtures/generic_identity_census, each a positive observation: a marked signature leaf; a minted container's renamed child; a call whose argument binds the parameter, observed typedIntwith no foreign parameter; the unobserved populations being declared; and the two supplied-node controls described under the review section below.head_of(xs: [1], d: 2)is reported asobserved unsubstituted,observed substituted, orcarrier unobservedwith the reason. It readsobserved unsubstituted, typed Ttoday. That is the spelling collision step 2 repairs, so the line is expected to flip and must not hold the standing hostage.v2.compiler.compile.The standing line, each control, the tallies and the unobserved rows are decided in
.dag. The host arm reads files, relays text, and maps the first line to a termination. That arm is admitted seed growth, declared ingunbc.generic_identity_census_seed_growthwith its trigger.src/v1/stage0/src/bin/generic_identity_census.rsis transport for any other subject (<receipt.tsv> <subject.dag>...).Evidence
Executed locally on this head, arm64, with a
gunbcbuilt from this tree:exit 0, followed by the report lines.
Mirrors: regenerated with
claim_executor --regen-round-cost --source-root dag --source-root src/v2in a standalone clone with its own target directory, looped torebuild_packages=0. On the first head the only path the round changed wasemitted_population.rs; on this head the round reportschanged_paths=0.Review on 1c3f45f (CHANGES REQUESTED), addressed in bc78f54 and d716390
The finding was that the reader turned absence of an observation into positive answers. Three changes:
gi_foreign_readinggainedForeignParameterValueArgumentUndecided; "no marked occurrence" no longer stands for "no occurrence".ResultCarrierObservationsays whether a call's result carrier was seen at all. The bound-call control holds only on a positive observation, and the collision reading is three-valued.gi_sig_rowsreads every signature.Then, in d716390, each new arm got an executed control over supplied nodes (DESIGN §4b: a state authorable at a fixture boundary is enrolled there):
owner_argument_arms_discriminate: one marked parameter,head_of'sd: T, is asked about under three owners built fromhead_of's real signature. As compiled it answersforeign_in_a_value_argument. With its value argument replaced by the list literal's type, whose element is spelledTand carries no mark, it answersforeign_value_argument_undecided. With no value argument it answersforeign_in_no_value_argument. The control holds only on all three.missing_carriers_are_unobserved: a name with no item, and the fixture's record declaration, which has no body, both answerResultCarrierUnobserved.Not covered, not verified
src/v1/05_emit_rust.dag. Re-running with that one file at its earlier revision reproduces 287,088, and every row that moves is inv1.compiler.emit_rust(closure_renders_async_trait_resource,emit_capability_method,emit_rust_selected). The first census binary, rebuilt and run on the current tree, gives the same rows as the current one.the_generic_identity_census_operand_routes_to_its_own_producerand clippy over the new host arm have not been run locally; CI is their first execution.🤖 Generated with Claude Code