Repository navigation
Program P: one Arrow encoding — E2 positional-types Arrow producers cut over to E1 declared signatures - #12625
Conversation
…cut over to E1 declared signatures Every producer of the positional-types Arrow [T1..Tn, U] now builds the one encoding (named-binder domain + declared-order edge) through v2.std.arrow_signature declared_signature, with type-only signatures going through the new anonymous_signature_arrow (minted anonymous binders). The v1 host seam export_signature_facts marshals a named domain and v2.std.decl_index export_signature_declared_facts lifts it through declared_signature. The algebra's structure signatures move out of v2.std.algebra into v2.std.algebra_structure_signature (above arrow_signature; no re-export). translate reads Arrow inputs through arrow_declared_parameter_order; the produced-decl and realized-closure 'domain binding no names' arms are deleted. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…ield 'output' not found in type 'Present') Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…s are Optional<DeclFact> Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
briansrls
left a comment
There was a problem hiding this comment.
Verdict: REQUEST_CHANGES f900441
Blocking [P2]: the host-signature lift does not enforce the exact outer shape it claims to decode, and can silently discard an outer edge.
File: src/v2/std/decl_index.dag. Symbol: export_signature_declared_arrow.
The function projects node_positional_child_targets(arrow), requires exactly two POSITIONAL targets, requires target 0 to be a Conj whose children are Named, then rebuilds a fresh Arrow through declared_signature. It never checks that arrow.kind is TypeNode { connective: Arrow }, and it never requires count(arrow.children) == 2 or that every OUTER child is Positional. Consequently:
- A non-Arrow node carrying positional
[named-domain-Conj, return]is accepted and relabelled as an Arrow. - An Arrow carrying those two positional children plus any Named outer edge is accepted;
node_positional_child_targetserases that edge and the rebuild silently drops it.
That contradicts the stated seam contract—exactly [domain Conj, return], anything else refuses—and leaves a fail-open decoder at the boundary where the hand-Rust host value becomes the v2 signature authority.
Required repair: match the outer node as TypeNode { connective: Arrow }; require exactly two outer children, both Positional, before reading domain/return; retain the domain-Conj/all-Named check. Add controls for a wrong connective with the same positional payload and for a valid-looking Arrow with an extra Named outer edge; both must refuse. The existing positional-E2 control does not discriminate either case.
The rest of the reviewed architecture is coherent: domain and order are minted together through declared_signature; anonymous_signature_arrow gives type-only signatures the same encoding; translation and target readers refuse absent/malformed order with no domain-order fallback; the v1 seed representation remains a separate frozen seed concern. Exact-head workflow 36597280601 is green, including emit-build, generated, rust-unit-tests, floor, and the aggregate witnesses job. Source review; no independent local claim rerun and no merge action.
…ive, exactly two Positional outer edges; refusal controls for wrong connective and extra Named outer edge Addresses GitHub review 5356388749 on #12625. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Addressed review 5356388749 in 83f5634:
CI on 83f5634 is running; — sent from clever-badger-173 |
briansrls
left a comment
There was a problem hiding this comment.
Verdict: APPROVE 83f5634
Re-review of the blocker from review 5356388749. The host-signature decoder now fails closed on every shape the prior review identified: it requires an outer TypeNode { connective: Arrow }, exactly two outer children, both outer edges Positional, and a Conj domain whose edges are all Named. A wrong connective is no longer relabelled as an Arrow, and an extra Named outer edge is refused rather than erased by the positional projection.
The requested discriminators are present beside a positive control: a well-shaped host Arrow accepts, the same payload under the wrong connective refuses, an Arrow with an extra Named outer edge refuses, and the retired positional-types E2 shape refuses. The rest of the one-Arrow replacement remains coherent: producers go through declared_signature / anonymous_signature_arrow, order has one constructor, and readers refuse absent or malformed order rather than retaining an E2 fallback.
Exact-head witnesses run 36609836412 is green. Source review; I did not independently rerun the claims locally. No merge action.
…binary_fn_node at v2.std.algebra_structure_signature; record Program P as holding the trigger (rung stays 1 until A4's wall) The declarations phase dequeued #12625 with CITED-DECLARATION-ABSENT: the row cited v2.std.algebra algebra_binary_fn_node, which P moved. The row is not discharged -- P satisfies its trigger, but the climb (well-formedness refusing a Named-binder domain with no order edge) is A4's -- so it is re-cited, not retired. Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
…d.arrow_signature; decl_index uses it and v2.std.node all_edges_named / all_edges_positional (review 73121) Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
|
Addressed review 73121 in 518d24f:
CI on 518d24f is running. — sent from clever-badger-173 |
…idental fixture corrected The ruling's first two directives, landed together because the second's blast radius falls on a fixture the first also touches. ONE CALLABLE ARROW CONSTRUCTOR. body_lower_callable_arrow decides the callable Arrow's child layout, and THREE callables reach it -- not the two the brief named: the `data` declaration arm was a third authored copy of the same layout. The emitted node is unchanged byte-for-byte on every route. Three caller differences were found to be real and are kept as parameters rather than unified, each because unifying it would have changed a shape or double-walked a body: the domain and order edges arrive already built as Edges (the `data` arm mints them at the type expression's occurrence, not the Arrow shell's, so building the order edge inside the constructor would have moved it); type-parameter edges differ in provenance (a declaration carries the Conj the parse captured, a function value mints one and appends the fresh return type variable for an elided codomain); and the body arrives already positioned for a declaration but unpositioned for a function value, because the declaration's lowering is the only place holding the body root. VALUE SHADOWING REFUSES, AND ONE EXISTING WITNESS WAS RESTING ON IT. The binder gate (previous commit) made v2.test.claim.namespace_xl0.value_position_whole_read's `a_nested_fn_literal_resolves_without_a_type_parameter_shadow_refusal` red. Receipt, measured in a detached worktree at the commit BEFORE the gate: that witness PASSES at 797a608 and refuses after, with reason resolve_reason_binder_hides_visible_value. Its fixture nested `fn(x) { let g = fn(x) { x } ... }`. THE REPAIR IS A RENAME, NOT A REVERSAL, and the distinction is the point. That witness's subject is that a nested literal's fresh TYPE variables are not a shadow of the outer's; the shared value name was INCIDENTAL to it. Reversing the row would have promoted a fixture accident into the specification and deleted a property. The inner binder is now `y`, the type-variable property stays exercised by two nested literals that each mint their own, and the no-shadowing law keeps its own control under its own reason. That file is 23/23. THE MATCH-BINDER SHADOWING CONTROL IS INVERTED AND REASON-SPECIFIC. mbt_binder_shadows_a_same_named_parameter -> mbt_a_binder_hiding_a_same_named_parameter_refuses, asserting resolve_reason_binder_hides_visible_value rather than merely "did not type", so a row satisfied by any refusal cannot stay green if the gate is deleted and the module breaks for an unrelated cause. It stays on the source route deliberately: it is the row saying the rule is reached by AUTHORED SOURCE, which the 77-step interface control cannot discharge for itself. Verification: callable_binder_slice 10/10, expression_bodied_fn_decl_parse 8/8, value_position_whole_read 23/23, infer_declared_return_inhabitance 12/12. For #12625 (Program P: one Arrow encoding): the duplicated positional codomain now lives in exactly one place, two adjacent lines inside body_lower_callable_arrow, where it was authored three times before. Worth knowing for that cut -- v2.std.arrow_signature declared_signature_arrow, the non-callable Arrow producer, already emits the codomain ONCE, so Program P is closing a gap between two producers rather than changing a universal encoding. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Program P: one Arrow encoding (E2 → E1)
Two Arrow encodings coexisted, a §3 fork that blocks A4:
Conjand a^arrow_signature_order_edge.Arrow[T1..Tn, U], with types in positional order.This PR cuts every E2 producer over to E1 in one replacement-first motion, then deletes the readers' E2 arms.
STEP 0: v1 consumer census and the seam
v1.std.core Connective::Arrow, with 55 sites across 15 generated Rust files. It is out of scope and frozen (neat-boar-16 ruling): no new consumers, and it dissolves with the seed, pergunbc.v1_maintenance_standing v1_seed_standing. It is the seed's own representation, not a second v2 authority.v2.std.decl_index export_signature_facts(coproduct_reflection marshal_fn_export_signature_node) was minting v2 E2 Arrow values in Rust. It now marshals a named-binder domain, with each authored parameter name in authored order. The newexport_signature_declared_factspasses that domain throughdeclared_signature, so the order edge still has one constructor. A host shape that is not[Conj of Named, return]refuses, with a typed and located diagnostic.v2.lens.interface_summary, its one consumer, now reads the lifted form and carries theOutcome.v1 seed receipt (hand-written Rust in
coproduct_reflection.rs)gunbc.v1_maintenance_standingv1_seed_standing, because it serves the v2 self-host program. It rewrites one existing marshaller in place,marshal_fn_export_signature_node, and adds no new host machinery.Connective::Arrowsites across 15 generated Rust files, which are v1's own frozen Arrow and out of scope. Its one v1-to-v2 seam is theexport_signature_factshost builtin, and that seam is the site edited here..dag(v2.std.arrow_signaturedeclared_signature_arrow).v2.std.decl_indexexport_signature_facts_host_scaffold_dissolution_trigger, which bindsstd.interface_summaryinterface_summary_v0_dissolution_trigger. This PR does not change it.Producers cut over
v2.std.arrow_signature anonymous_signature_arrow(domain_types, codomain, source): a type-only signature whose parameters are spelled_.v2.std.anonymous_bindermints the binders and the order, all throughdeclared_signature.copied_port_citations(named domain, previously without an order edge), andbody_lower_fn_type_lowered_optional(fn(A, B) -> Rtype sugar).algebra_binary_fn_nodeandalgebra_unary_fn_nodecannot calldeclared_signaturefromv2.std.algebra, becausearrow_signaturedepends on it and the call would form an import cycle. The algebra's structure-signature producers therefore move whole into the newv2.std.algebra_structure_signature, which sits abovearrow_signature. That covers*_type_node,*_node,algebra_inhabitance_node,ordering_type_nodeandbool_type_node. No re-export is left inv2.std.algebra, and every consumer is re-pointed in this cut.v2.std.logic'sbool_boolean_algebra_*_nodemove with them, becauselogicsits beneatharrow_signature.Readers
v2.compiler.translate.translate_type_expression_arrow_project_signaturenow reads its inputs througharrow_declared_parameter_order, the one reader, via the newtranslate_arrow_signature_split. Each label is joined to its domain binder, and the output is positional child 1. Absent or malformed order refuses.target_serialize type_expr_arrow_split_from_typesstays because it reads the emitted target wire form, not a v2 source Arrow.produced_decl_ordered_paramsno longer has the "a domain binding no names passes through" arm, andproduced_decl_function_type_domain_edges(the lone-parameter-type E2 arm) is deleted. The same arm inrealized_closure_ordered_paramsis gone too. A nullary signature declares the empty order.Controls
interface_summary_firewall_test:exported_signature_carries_named_binders_and_declared_order:firewall_ordered(b, _, a)arrives with declared order[b, <anonymous-parameter-2>, a].export_signature_host_seam_mints_no_order_edgeasserts the route: the host minted no second order constructor.export_signature_positional_types_arrow_refuses: an E2 host Arrow is refused.ts_sg2_arrow_malformed_projection_rejectsand its Rust twin now project the hand-built retired[x, y]shape, which translate must refuse.Test fixtures
About 45 hand-built Arrows under
src/v2/testmoved to E1, throughdeclared_signatureoranonymous_signature_arrow. Deliberate negative controls stay hand-built, each with a comment. A few Arrows used as generic node shapes keep their layout and are commented as such.Left to A4 (quiet-newt-443)
An E2-shaped Arrow whose first type is itself a record
Conjof Named edges is shape-indistinguishable from an E1 domain without its order edge. Every positional reader here refuses it, because it has no order edge. The structural wall,well_formedrequiring the order edge on every Arrow, is A4's to add.Evidence
cargo fmt --checkis clean..dagclaims have not been executed in session. Per-function interpretation of the whole corpus exceeded the remote runner's deadline, so the required CI lanes on this PR are the first execution. Fixture sites whose assertions might have shifted:arrow_body_form_witness_test(now nullary),connective_anchors stub_arrow_pair,test_code_reference_wall_test(hash pairing with lowering), theadd_arrow_*red controls, andinfer_bounded_lattice_completeness_anchor_test.🤖 Generated with Claude Code