Skip to content

Prove extension calibration nodes' measurement producers in compose - #1488

Merged
MaxGhenis merged 6 commits into
mainfrom
be/a-composed-proofs
Nov 4, 2026
Merged

MaxGhenis merged 6 commits into
mainfrom
be/a-composed-proofs

Conversation

@MaxGhenis

@MaxGhenis MaxGhenis commented Nov 3, 2026 •

Copy link
Copy Markdown
Contributor

This PR targets main. It stacked on #1486 (nzhub/g8r2c-g-fix1), the NZ hub's E–G fix round, until G (#1478) landed on main as f8f543a4. The branch forks from 20507ad8, an ancestor of G's head. d66cf707 merges main into it after G, and b536dd29 merges main again after H2 (#1485) and #1501. The NZ hub clears it.

What changes

measurement_proofs reads only the declared graph's rows, so the declared proof never names a calibration node that a transport extension adds. One example is the calibrate.* node of a calibration-tier scenario, which the entitlement factory in T/entitlement.py builds from the scenarios resource. And the extension pass of compose_transport_graph reruns the ancestry guard on the extended graph but never ran _check_measurement_proofs. So a scenario's calibration node could calibrate against a money-scaled measurement that no proof covered.

The extension pass now runs _check_measurement_proofs right after its ancestry guard, as the skeleton pass does. For a calibration node that an extension adds, the compiled graph proves the producer:

  • exactly one compiled ancestor declares the measurement (R2C-1);
  • that ancestor outputs every proof column (R2C-1);
  • no other compiled ancestor writes a proof column, by output or EXPAND cell (R2C-15).

The refusal names the node as an extension calibration node with no proved producer. Each skeleton calibration node keeps the declared comparison, which the pass now also runs on the extended graph.

The compiled check also refuses a malformed measurement_id, as the declared check does. When any declared row's measurement_id is neither null nor a nonempty string, measurement_proofs parks every measurement. When the declaration proves at least one measurement, _check_measurement_proofs now refuses composition if a node of the compiled graph has such an id, with the declared check's reason, before it proves any producer. It reads an explicit null as no declaration. When the declaration proves none, the check returns before this scan, as it returns before every other step. Before, an extension node with measurement_id: 7 beside the string producer composed.

T/ = packages/microcosm-build/src/microcosm/build/transport/.

Invariant

For every calibration node of the composed graph, skeleton or extension, and each proved measurement: exactly one compiled ancestor declares the measurement, that ancestor outputs every proof column, and no other compiled ancestor writes one. At a skeleton node, that ancestor is the declared proof's producer. And a composed graph that proves a measurement holds no node whose measurement_id is neither null nor a nonempty string.

Tests

test_transport_measurement_proof.py:

  • Unit cases on the compiled toy, with a proof that names no calibration node and toy.calibrate passed as an extension node. One declarer passes, alone or beside an EXPAND of another column. No declarer, two declarers, a missing universe column, an EXPAND of the income and a later-version rewrite of the income each refuse, the rewrite with its exact message. The same proof still refuses at a skeleton node, and naming other nodes as extension nodes leaves the skeleton's checks as they were.
  • Differential property. Take chains of nodes that each may declare the measurement and may write the income and universe columns. The declared proof (measurement_proofs on the rows) and the compiled extension proof agree on each chain, refusal for refusal: the same verdict, and the same text apart from the missing-column clause's wording. Hypothesis draws 60 chains of up to four nodes, plus five fixed examples. Outside the suite I ran all 4,680 such chains: no disagreement, and every branch reached (10 pass, 939 missing columns, 303 second writers, 340 with no declarer, 3,088 with two or more).
  • Malformed ids. One declarer's chain, plus another node upstream of calibration whose measurement_id is 7, "" or None. The test runs the declared check and the compiled check at an extension calibration node and at a skeleton one. Both refuse 7 and "" with the same reason, and both ignore None. Without the last commit's compose change, the compiled check accepts the four 7 and "" cases, and they fail.

test_nz_transport_toy_graph.py, the NZ hub's file, since the hub owns the toy and its node ids:

  • NZ's synthetic graph (make_nz_toy_fixture), whose V1, V3 and VHF scenarios calibrate. It composes, and the declared proof doesn't name nz.v.V3.calibrate. Five V3 mutants refuse, each naming nz.v.V3.calibrate. The declaration still proves the measurement in each, so only the extension pass can refuse:
    • M1: V3's stand-in keeps its outputs and drops measurement_id (no declarer);
    • M2: V3's earnings node declares the measurement too (two declarers);
    • M4: V3's universe column moves from the stand-in to the earnings node (the one declarer doesn't write it);
    • G7, the NZ hub's shape, in two placements (two writers). A filter version inside V3 rewrites both measured columns and takes preparation, the compiled targets and the problem. In the first, V3's calibration opens from that version, so the rewrite joins its base. In the NZ hub's placement, the calibration keeps its base on V3. The problem reads the rewritten columns, so only the calibration's artifact edge from the problem reaches the rewrite.

At 20507ad8, without the compose change, the shared file fails the 15 tests that pass extension_nodes: each stops on the missing keyword. NZ's file fails the five mutant cases, because each mutant composes there.

Seven hand mutants of the hunk each fail at least one of the two files:

  • dropping the extended-pass call: NZ's file (the five mutant cases compose);
  • passing no extension nodes: NZ's file (the toy itself stops composing, because V1's calibration meets the declared comparison and refuses);
  • treating every calibration node as an extension's: the shared file (five tests);
  • dropping the column check, letting two declarers pass, or skipping the writer rule for extension nodes: both files;
  • following no artifact edges in the closure: NZ's file alone, through G7 in the NZ hub's placement. Every other test passes under this mutant, the first G7 included.

NZ's packaged graph

Outside the suite, I composed NZ's packaged graph (_nz_composition_spec_and_config from test_nz_transport_declarations.py) and mutants of it, at 20507ad8, bdc75bd5 and b64eb6c2.

My mutants edit the spec that _nz_composition_spec_and_config returns. By then NZ's shims have run, among them add_measurement, which adds a synthetic declarer to each calibration scenario whose rows declare no measurement. So my M1 leaves VSI with no declarer. In the NZ hub's brief 216, M1 went through that function, so the shim fired: it adds nz.v.VSI.synthetic_measurement, which declares the measurement and outputs the same three columns, and composition refuses with a GraphError, since two nodes own person.ird_taxable_income_proxy_cents in nz.v.VSI. I reran that build, editing the rows before the shims run, at 20507ad8 and at b64eb6c2, and got 216's refusal at both. The toy's M1, in test_nz_transport_toy_graph.py, reaches the zero-declarer branch, and the test asserts that refusal.

Graph 20507ad8 bdc75bd5 and b64eb6c2
NZ's packaged graph, 9 calibration nodes composes composes
M1: VSI's stand-in drops measurement_id, after NZ's shims have run composes refuses: 0 declarers upstream of nz.v.VSI.calibrate
M2: VEX's benefits.annual_transfers declares the measurement too composes refuses: 2 declarers upstream of nz.v.VEX.calibrate
M4: VEX's universe column moves to benefits.annual_transfers composes refuses: nz.v.VEX.income.standin doesn't write it
G7: a filter version inside VEX rewrites both measured columns, and nz.v.VEX.calibrate opens from it composes refuses: writers nz.v.VEX.income.standin and nz.v.VEX.review.rewrite
G7 in the NZ hub's placement: the same version, with nz.v.VEX.calibrate left on nz.v.VEX composes refuses: the same two writers
Both G7 placements inside VSI compose refuse: writers nz.v.VSI.income.standin and nz.v.VSI.review.rewrite

The rewrite's node id, nz.v.<V>.review.rewrite, comes from my probe; the NZ hub's brief 216 names that node nz.v.VSI.review_rewrite.

In the NZ hub's placement, only the calibration node's artifact edge from targets.problem puts the rewrite among its compiled ancestors. I rebuilt each mutated graph with every node's artifact inputs removed and compiled it again. In the NZ hub's placement, the calibration node's closure then lacks the rewrite; in the other placement, it still holds it. The same held on the toy's V3.

Reach

  • Tests. At bdc75bd5, I ran the 27 test files that reach compose or its fixtures, serially: 3,239 passed, 34 skipped, 0 failed. 32 skips need BE_CHRONICLE_ARTIFACT, and 2 need a staged pinned feed. The NZ hub ran its declarations and entitlement-graph files with its pinned feed at bdc75bd5: 129 passed, none skipped. At 3196273c, the NZ hub's brief 216 ran NZ's six files: 719 passed, against 703 at 20507ad8, with no skips; only the 16 tests this PR adds differ. At b64eb6c2, I ran these serially:

    File Passed Skipped Failed
    test_transport_measurement_proof.py 49 0 0
    test_nz_transport_toy_graph.py 37 0 0
    test_transport_composed_graph.py 469 0 0
    test_transport_evidence_kernels.py 156 0 0
    test_transport_holdout_separation.py 41 0 0
    test_be_target_references.py 156 32 0
    test_transport_run_entry_factors.py and test_transport_run_entry_forms.py 304 0 0
    test_calibration_columns.py 88 0 17

    The 32 skips need BE_CHRONICLE_ARTIFACT. The 17 calibration-column failures ("Interval outputs need the effective interval document") fail the same way at 3196273c and at 20507ad8, so this PR doesn't cause them. On main after G, they pass (next item).

  • Merge. b64eb6c2 merges with no conflict into main (79a533c7), into G's head (f43e8fbb), and into a scratch merge of f43e8fbb into 79a533c7. That scratch merge has tree 49f82adf, the same tree as main now that G has landed (f8f543a4). Merged with b64eb6c2, it gives tree 57481e8f, which d66cf707 and this PR's merge ref (298e8baf) also have. On 57481e8f: test_transport_measurement_proof.py 49 passed, test_nz_transport_toy_graph.py 37 passed, test_calibration_columns.py 106 passed, test_transport_evidence_kernels.py 156 passed, and test_transport_composed_graph.py 469 passed.

  • Kernels. None of the 45 toy-registry kernel hashes, or the 3 simulate.* hashes under AxiomEngine, moved from 20507ad8 to bdc75bd5 or from 3196273c to b64eb6c2. The NZ hub's run agrees for 3196273c.

  • US. The primary-QRF worker identity is byte-identical at 20507ad8 and bdc75bd5, and at 3196273c and b64eb6c2.

  • After H2 and Tighten five G tests that checked less than their names claim #1501. b536dd29 merges main e2918f4f, which holds H2 (Bind NZS co-residence from household composition (H2) #1485) and Tighten five G tests that checked less than their names claim #1501. git merge-tree reports one conflict, at the end of test_nz_transport_toy_graph.py, where H2's section and this PR's both append. The resolution keeps main's file whole, Tighten five G tests that checked less than their names claim #1501's middle edits and H2's section included, and appends this PR's section: blob 5cb8c87c, the blob the NZ hub named. Against main, the PR still changes the same four files. T/compose.py, test_transport_measurement_proof.py and the changelog fragment keep their patch-ids, and the toy file adds the same 158 lines and removes none. No top-level name repeats in the resolved file, so no test shadows another. On the head's tree, I ran these serially:

    File Passed Skipped Failed
    test_transport_measurement_proof.py 49 0 0
    test_nz_transport_toy_graph.py 40 0 0
    test_transport_composed_graph.py 469 0 0
    test_transport_evidence_kernels.py 156 0 0
    test_transport_holdout_separation.py 51 0 0
    test_calibration_columns.py 106 0 0
    test_transport_graph.py 15 0 0
    test_transport_compile_modules.py 11 0 0
    test_first_party_imports.py 6 0 0
    test_nz_spec_package.py 1,203 0 0
    test_nz_target_references.py 20 41 0
    test_nz_transport_declarations.py 60 2 0

    Skips: 41 in test_nz_target_references.py (NZ_CHRONICLE_ARTIFACT is unset; public NZ feed audit unavailable); 2 in test_nz_transport_declarations.py (Pinned feed not staged).

    test_nz_spec_package.py lists the checkout's files with git ls-files, so it ran in a scratch git repository whose index reproduces the head's tree hash; every other file ran on a git archive copy.

    From e2918f4f to b536dd29, none of the 48 kernel hashes moves, and the US primary-QRF worker identity stays byte-identical.

  • After Encode person_role bindings and their closure defaults on the person table (S2b PR 2) #1480. Encode person_role bindings and their closure defaults on the person table (S2b PR 2) #1480 landed as 6448792c after CI run 41887093744 had tested this PR on e2918f4f. The two PRs share no file. git merge-tree merges b536dd29 with 6448792c cleanly, into tree cca924f0, which adds to the head's tree exactly what 6448792c adds to e2918f4f: the same five files, with the same patch-id. On cca924f0, I ran both PRs' test files and the composed graph, one at a time:

    File Passed Skipped Failed
    test_transport_measurement_proof.py 49 0 0
    test_nz_transport_toy_graph.py 40 0 0
    test_transport_column_kernels.py 36 0 0
    test_concept_mapping.py 266 0 0
    test_group_encode.py 82 0 0
    test_transport_composed_graph.py 469 0 0

Before ready

  • Reach at b64eb6c2: the tests above, the 48 kernel hashes and the US worker identity.
  • An independent review (r2) of 20507ad8..3196273c: approve, with one low finding and one prose note, which b64eb6c2 answers.
  • The NZ hub's clearance at 3196273c (brief 216: clear, with nits). This body fixes nit 1; the NZ hub makes nits 2 and 3 in its own PR after this one lands.
  • The NZ hub's clearance of b64eb6c2, by reading: the compiled rule mirrors the declared one, and every NZ measurement_id is a nonempty string, so the new refusal can't fire on NZ's graphs. It holds on the condition that CI passes on this PR merged with main after G.
  • An independent review (r3) of b64eb6c2: approve, with one note: the compiled check scans for malformed ids only when the declaration proves a measurement. 325ee9a8 puts that condition in the docstring, and this body states it too. d66cf707 adds only the merge of main.
  • G lands (f8f543a4), this PR retargets to main, and d66cf707 merges main in.
  • CI passes on the merge ref 298e8baf (f8f543a4 plus d66cf707): run 41746690305.
  • H2 (Bind NZS co-residence from household composition (H2) #1485) and Tighten five G tests that checked less than their names claim #1501 land first, by agreement with the NZ hub: H2 as 358b1c16, Tighten five G tests that checked less than their names claim #1501 as e2918f4f. Both edit test_nz_transport_toy_graph.py, so b536dd29 merges main and keeps every change to that file: Tighten five G tests that checked less than their names claim #1501's edits in its middle, H2's appended section, then this PR's. CI passes on the merge ref 8b7752ee (e2918f4f plus b536dd29): run 41887093744.
  • The NZ hub's clearance of b536dd29: land it once CI passes and the local runs agree.

🤖 Generated with Claude Code

The extension pass of compose_transport_graph compiled the extended graph
and reran the ancestry guard, but never ran _check_measurement_proofs. So a
calibration-tier scenario's calibrate.* node could calibrate against a
money-scaled measurement that no proof covered: measurement_proofs reads
only the declared graph's rows and never names those nodes.

The extension pass now runs the check after the ancestry guard, as the
skeleton pass does. For a calibration node that an extension adds, the
compiled graph proves the producer under R2C-1's rule: exactly one compiled
ancestor declares the measurement, and that ancestor outputs every proof
column. R2C-15's only-writer rule applies as before. A skeleton calibration
node keeps the declared comparison, which the pass now also runs against
the extended graph.

Tests: unit cases on the compiled toy; a differential property that the
declared proof and the compiled extension proof agree, refusal for refusal,
on chains of declarers and writers; and NZ's synthetic graph with four V3
mutants (M1, M2, M4 and the NZ hub's G7), each of which composes without
this change.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@MaxGhenis
MaxGhenis changed the base branch from nzhub/g8r2c-g-toy to nzhub/g8r2c-g-fix1 November 3, 2026 10:54
The five tests that run the extension proof on NZ's synthetic graph name the
toy's V3 nodes, and the NZ hub owns the toy and its node ids. They move, with
their helpers, from test_transport_measurement_proof.py into
test_nz_transport_toy_graph.py and use that file's module `toy` fixture, so a
change to the toy edits only NZ's files. The shared file keeps the unit tests
on the compiled toy and the differential property.

The move adds G7 in the NZ hub's placement. V3's calibration keeps its base on
V3, while preparation, the compiled targets and the problem move into the
review version that rewrites both measured columns. The problem reads the
rewritten columns, so only the calibration's artifact edge from the problem
puts the rewrite among its compiled ancestors. The earlier G7 opens the
calibration from the review version, where the rewrite joins its base, and
doesn't need that edge.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Review r2 found that the compiled check skipped a node whose
measurement_id was neither None nor a nonempty string, while the declared
check refuses it. With the string producer still in place, an extra
upstream node declaring measurement_id 7 composed, though the same param on
a declared row parks every measurement. r2 showed it on NZ's toy graph,
where V3's earnings.cents with id 7 composed.

_check_measurement_proofs now refuses such a node with the declared
check's reason before it proves any producer, and reads an explicit None as
no declaration, as measurement_proofs does.

The new test gives a node upstream of calibration a measurement_id of 7, ""
or None, and runs the declared check and the compiled check on a
calibration node that an extension adds and on a skeleton one. Both checks
refuse 7 and "" with the same reason, and both ignore None. Without the
fix, the compiled check accepts the four 7 and "" cases, and those cases
fail.

The commit also fixes three docstrings that r2 flagged: the test module's
account of the compiled tests, which patch in a proof; _chain's, whose
nodes chain by step columns; and compose's module docstring, which now
names gate_inputs, the other explicit way an extension may add a skeleton
predecessor.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@MaxGhenis
MaxGhenis changed the base branch from nzhub/g8r2c-g-fix1 to main November 4, 2026 00:24
MaxGhenis and others added 3 commits November 3, 2026 19:25
G landed on main as f8f543a, and this PR now targets main. After the retarget, GitHub's merge ref kept G's old branch head f43e8fb as its first parent, so this merge starts CI on main as it now stands. The merge writes the tree git merge-tree gives for main and b64eb6c, 57481e8, where the measurement-proof, NZ toy-graph, calibration-column, evidence-kernel and composed-graph test files all passed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
_check_measurement_proofs returns before its malformed-id scan when the declaration proves no measurement, and its docstring now says so. The independent review of b64eb6c noted that the sentence read as unconditional.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
H2 and #1501 landed on main, and both change test_nz_transport_toy_graph.py, as this PR does. git merges every other file without a conflict. The one conflict sits at the toy file's end, where H2's section and this PR's section both append. The resolution keeps main's file whole, #1501's edits included, then appends this PR's section unchanged: blob 5cb8c87. This PR's diff against main still adds the same 158 toy-file lines in the same order, and its other three files keep their patch-ids. No top-level name in the resolved file repeats.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@MaxGhenis
MaxGhenis marked this pull request as ready for review November 4, 2026 20:34
@MaxGhenis
MaxGhenis merged commit 3e7a704 into main Nov 4, 2026
11 checks passed
@MaxGhenis

Copy link
Copy Markdown
Contributor Author

Landed as squash 3e7a7045 on main, from head b536dd29 (gh pr merge --squash --match-head-commit).

At merge time:

  • CI: run 41887093744 passed all 11 checks on b536dd29, which merges main e2918f4f into the branch. The PR's merge ref 8b7752ee had e2918f4f as its first parent and the head's tree (5df87403).
  • Reviews: two independent reviews approved, both GPT-6.1 Sol through Subfleet. r2 (20261103-072635-be-a-proof-review-r2, codex-5) approved 3196273c with one low finding and one prose note, which b64eb6c2 answers. r3 (20261103-181116-be-a-proof-review-r3, codex-6) approved b64eb6c2 with one note: the compiled check scans for malformed ids only when the declaration proves a measurement. 325ee9a8 says so in the docstring, and the body says it too. No review asked for changes, and GitHub reported the PR mergeable.
  • The NZ hub cleared 3196273c (brief 216, with nits: the body fixes nit 1, and the hub makes nits 2 and 3 in its own PR). It cleared b64eb6c2 on the condition that CI passes on this PR merged with main after G, which run 41746690305 met on d66cf707. At 18:31Z it cleared b536dd29: land it once CI passes and the local runs agree.
  • Since b64eb6c2, three commits reached the branch: d66cf707 merges main f8f543a4 (G), and its tree equals git merge-tree's; 325ee9a8 edits only _check_measurement_proofs's docstring; b536dd29 merges main e2918f4f (H2 Bind NZS co-residence from household composition (H2) #1485 and Tighten five G tests that checked less than their names claim #1501). Of this PR's four files, main changed only test_nz_transport_toy_graph.py in that span. b536dd29 resolves that file's one conflict by keeping main's file whole and appending this PR's section (blob 5cb8c87c, the blob the NZ hub named). The squash's parent is main 6448792c (Encode person_role bindings and their closure defaults on the person table (S2b PR 2) #1480's squash).
  • Locally, on the head's tree, these files passed, one per process: test_transport_measurement_proof.py (49), test_nz_transport_toy_graph.py (40), test_transport_composed_graph.py (469), test_transport_evidence_kernels.py (156), test_transport_holdout_separation.py (51), test_calibration_columns.py (106), test_transport_graph.py (15), test_transport_compile_modules.py (11), test_first_party_imports.py (6), test_nz_spec_package.py (1,203; in a scratch git repository whose index reproduces the head's tree), test_nz_target_references.py (20; 41 skipped without NZ's feed) and test_nz_transport_declarations.py (60; 2 skipped without the pinned feed). From e2918f4f to b536dd29, none of the 48 kernel hashes moves, and the US primary-QRF worker identity stays byte-identical.
  • After Encode person_role bindings and their closure defaults on the person table (S2b PR 2) #1480. Main moved to 6448792c (Encode person_role bindings and their closure defaults on the person table (S2b PR 2) #1480) after CI ran. The two PRs share no file. git merge-tree merges b536dd29 with 6448792c cleanly, into tree cca924f0, which adds to the head's tree exactly what 6448792c adds to e2918f4f: the same five files, with the same patch-id. On cca924f0, these files passed, one per process: test_transport_measurement_proof.py (49), test_nz_transport_toy_graph.py (40), test_transport_column_kernels.py (36), test_concept_mapping.py (266), test_group_encode.py (82) and test_transport_composed_graph.py (469). The squash's tree is cca924f0, the tree these runs used.

@MaxGhenis
MaxGhenis deleted the be/a-composed-proofs branch November 4, 2026 20:37
MaxGhenis added a commit that referenced this pull request Nov 4, 2026
Since the merge base 875506e, main gained #1473, #1506, H2 (#1485),
#1501, #1480 and #1488. The merge is clean. Two files changed on both
sides, in separate hunks: compose.py (#1488 on main's side) and
test_transport_evidence_kernels.py (H2 on main's side).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MaxGhenis added a commit that referenced this pull request Nov 5, 2026
…losure (S2b PR 1) (#1482)

* Add binding-local views to the Axiom adapter

AxiomEngine takes an optional views sequence of AxiomView declarations:
a logical engine entity no frame entity maps to (rulespec-be's Child), one
bool person selector column, and an outside value per output. The adapter
gathers the selected person rows in table order, runs the module's program
on the logical entity, checks the engine's array against the selected count,
and scatters it back through the same mask; every other row holds the
outside value, cast through the output's graph dtype. An empty selection
makes no engine call, and a null or non-bool selector refuses.

View outputs resolve to the person entity, so callers that key on
(binding entity, variable) read them unedited. Each view's program compiles
under its own cache key, re-checks the pinned RuleSpec tree first, refuses
dense relations, and contributes its derived metadata, so a Child-only
module has metadata. The selector joins the person entity's
relation_dependencies; view_root_inputs() reports each view's roots.
axiom_engine_ref writes views only when present, so every existing
reference is unchanged. The view code stays in axiom.py, because
source_hash hashes defining files and does not follow imports.

* Partition binding-local view roots in the input closure

closure_partition no longer refuses a binding that declares views, and
BINDING_LOCAL_VIEW_MESSAGE is gone. Per binding, each view's logical entity
(Child) joins the live entities and maps to the person table, so a view's
roots partition against the closure's Child entries and the existing frame
check reads them on the person slice. Roots on that entity stay unmapped on
every other binding, and unreached_roots still reads only the binding's
engine entity, so it cannot excuse a view root.

engine_root_inputs adds each view's roots under its logical entity through
AxiomEngine.view_root_inputs(), and refuses a view binding on an injected
adapter. binding_view_entities reads a binding's logical entities for the
closure and compose.

* Parse binding-local views in the registry and check them in compose

The registry parses a binding's views block into AxiomView declarations
(logical_entity, selector {column}, outside {name: value}) and builds the
adapter with them. It refuses an empty list, views beside relations, a
binding off the person entity, a logical entity that names a mapped engine
entity, a repeated logical entity, a selector with any field but column, a
structural selector, a selector that names a binding output, and an outside
key that names no binding variable. Once the adapter is pinned, it checks
each view's program for relations in place of the binding entity's program,
requires each view's outside keys to equal the binding's variables on its
logical entity, and refuses a view input named like a root input of the
binding entity's program. _check_engine compares an injected adapter's views
with the binding's and refuses views on an injected Python adapter.

binding_view_dependencies reports each selector as a whole-table person
slice, the same columns AxiomEngine.relation_dependencies reports to the
rules kernels. Compose unions them with the relation dependencies for every
rules node, refuses a view node whose person slice omits an input the
closure encodes (other than through a graph node) or defaults on the view's
logical entity, and requires each selector on the closure producer's person
slice.

* Pin NZ-shaped and relation engine references to goldens from the base

No NZ CI test builds an axiom_engine_ref for NZ's rows: NZ's engine-free
graph injects Python toy engines. The new golden holds references generated
at main 4a36edc for NZ's six binding rows (unreached_roots included) over a
synthetic tree, and for the registry and adapter relation fixtures, all
built engine-free through build_transport_registry and axiom_engine_ref.
The test compares them byte for byte, so a reference that gains
"views": [] or "views": null without a declared view fails.

A second test, gated on POPULACE_RULESPEC_NZ, builds NZ's six real
references from the tree alone and compares them with a frozen copy the NZ
hub writes at the base.

* Add the changelog fragment for binding-local views

* Test that every rules kernel requires a view's whole selector slice

SimulateRulesKernel._require_relation_inputs reads the adapter's
relation_dependencies, which now carry each view's selector, so a node
whose person slice omits or masks the selector refuses before the engine
runs. The test pins that path for a view adapter.

* Pin view code to axiom.py and the no-view outputs to the base path

The placement lint now walks every import node in axiom.py, relative and
function-body imports included, and a second test requires AxiomView and
every view helper to carry axiom.py's module name. A helper moved into a
module axiom.py already imports (materialize, concept_mapping) would leave
the simulate.* hashes unmoved by an edit to it; the module-name test
refuses that move, which the import pin alone passes.

P4 gains an output clause: with views=None, materialize returns the same
names, order, dtypes and values, through the same engine calls, as a
reference copy of main 4a36edc's no-view path kept in the test. NZ's CI
graph injects toy engines and never runs AxiomEngine.materialize, so this
is the executable guard on view-free outputs.

* Class a view's defaulted roots as person columns in the support roster

_support_roster mapped each defaulted closure entry to a frame entity
through entity_names alone, so a defaulted Child root, which PR 2 writes on
the person table, mapped to no entity and missed the closure_default class.
_closure_defaults now maps a binding-local view's logical entity to the
person entity for entries of that binding's module. Without views the
mapping is unchanged.

* Freeze NZ's real-tree engine references at the base

test_nz_real_refs_match_their_frozen_copy compares NZ's six real
references with a frozen copy, and wrote none without a rulespec-nz
tree. This adds the copy, generated at PR 1's base (main 4a36edc) from
a git archive of rulespec-nz 8dc2507d, the commit NZ's bindings pin.

The base run froze the file, and a second base run passed against it.
At this branch's head the test passes too, so the six references keep
their bytes with views in place. The CI golden test passed at the base
as well, which checks that axiom_engine_refs.json came from the base.

* Document binding-local views in the declared-units guide

The guide said binding-local views remained separate work. It now
describes the declaration, the gather and scatter, the outside values,
the registry's refusals, the selector slice, the closure's treatment of
view roots, and the row-locality assumption that the skip-gated
real-engine differential tests.

* Union shared-path closure roots to remove binding-order dependence

* Cover both logical views to catch dropped input roots

* Validate complete outside declarations before pinning bindings

* Preserve outside value types in view equality and hashing

* Exercise view property edges across every graph dtype

* Type and stabilize real Child differential inputs

* Freeze CI reference bindings to isolate NZ edits

* Clarify view evidence, serialization and selector refusals

* Accept overrides of a view selector that a program reads

The first review of the fix round (P2) found that 0d6201a's selector
refusal also refused an override of a selector that a Person program
reads as a root input. The registry accepts that shape, variables()
lists the selector, and before 0d6201a the counterfactual bridge
applied such an override. validate_input_override now names a selector
only when no program reads it, which is exactly when the bridge refuses
the override as outside the engine's inputs, so the check changes no
override the bridge applies.

test_a_selector_that_a_program_reads_stays_overridable drives the
counterfactual bridge with a Person program that reads is_child: the
override reaches that program's input and the rows the view selects. It
fails on 0d6201a's check. The refusal test now also runs through the
bridge, which calls no program. The guide states the rule.

* Correct the two docstrings that review B flagged

`_real_inputs` said the pinned engine refuses a wrong-typed input by name.
At axiom-rules-engine 753ce7d, `src/dense.rs` reports a bool, text or date
column as a type mismatch when a program needs a number from it ("expected
decimal-compatible dense column" for an arithmetic operand, "{side} side of
comparison is not numeric" for a comparison), and neither message names the
input. The docstring now says that.

`axiom_ref_goldens.py`'s module docstring wrote `"\n"` in a non-raw string,
so it rendered a line break where the regeneration recipe needs the two
characters. It now escapes the backslash.

Two merges of main bring this branch up to date: `02265bb5` merges main `875506e8`, and `36800b14` merges main `3e7a7045` (#1473, #1506, H2 #1485, #1501, #1480 and #1488). git merged both without conflicts.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
MaxGhenis added a commit that referenced this pull request Nov 5, 2026
Tighten NZ's ageing and declarations tests after #1488 and #1507
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