diff --git a/docs/measurements/precondition-state-isolation-20261025.json b/docs/measurements/precondition-state-isolation-20261025.json new file mode 100644 index 00000000..25924a80 --- /dev/null +++ b/docs/measurements/precondition-state-isolation-20261025.json @@ -0,0 +1,130 @@ +{ + "measurement_date": "2026-10-25", + "base_commit": "9eb4f320d3db34d372145261704b805b88e39bda", + "base_source_sha256": "b32c83db3546567b3a5bc4d8b6a589a862c39b5fb59bd284b885d72e47d47a68", + "fixed_source_sha256": "af6a2d33b7aff2f09260144dd73a828910357e520be259995c5a2d529b719f7a", + "fixture": { + "common_record": { + "time": 0, + "process_id": 1, + "thread_id": 2, + "function": "fixture.step" + }, + "A": { + "positive": { + "meta_vars.phase": "train", + "meta_vars.signal": true + }, + "negative": { + "meta_vars.phase": "train", + "meta_vars.signal": false + } + }, + "B": { + "positive": { + "meta_vars.phase": "train" + }, + "negative": { + "meta_vars.phase": "eval" + } + }, + "expected_A_clause": { + "prop_name": "meta_vars.signal", + "type": "constant", + "values": [ + true + ] + }, + "expected_B_clause": { + "prop_name": "meta_vars.phase", + "type": "constant", + "values": [ + "train" + ] + } + }, + "fresh_process_sequences": [ + { + "order": [ + "B" + ], + "before_counts": [ + 1 + ], + "after_counts": [ + 1 + ], + "python_random_state_unchanged_before_and_after": true + }, + { + "order": [ + "A", + "B" + ], + "before_counts": [ + 1, + 0 + ], + "after_counts": [ + 1, + 1 + ], + "python_random_state_unchanged_before_and_after": true + }, + { + "order": [ + "B", + "A" + ], + "before_counts": [ + 1, + 1 + ], + "after_counts": [ + 1, + 1 + ], + "python_random_state_unchanged_before_and_after": true + }, + { + "order": [ + "B", + "B" + ], + "before_counts": [ + 1, + 1 + ], + "after_counts": [ + 1, + 1 + ], + "python_random_state_unchanged_before_and_after": true + } + ], + "regression_tests": { + "total": 6, + "before_failures": 5, + "before_passes": 1, + "after_passes": 6 + }, + "coverage": [ + "independent and reversed order", + "repeated independent solves", + "explicit set updated and reused", + "recursive sibling sharing with distinct root sets", + "fresh versus warm process histories" + ], + "limits": [ + "No multi-worker-count scheduling matrix measured.", + "No global inference ordering or scheduling determinism claim.", + "No unchanged large-trace output claim; fixing leakage may recover additional preconditions and change inference outputs.", + "Independent correctness fix; not part of the identity-cache performance comparison." + ], + "evidence_sha256": { + "before.json": "cb4fe5ac7cdb5ebe1544dc61ec06ed18de2a435cba2fad2d33fbbfb4ac022119", + "after.json": "62beead0bab542c5b7961588ed99d8c0977696169caacbca77d845c0b74e1383", + "tests-before.log": "970f9696404be2409515ab16d0a44d452e3a82d4d85acfb42844ef3b8f23b0d5", + "tests-after.log": "bebcffb3ddb091ef39bac8cfea9085bbe09e97363ba67c01acd50c3821e1096d" + } +} diff --git a/docs/measurements/precondition-state-isolation-replay-20261025.json b/docs/measurements/precondition-state-isolation-replay-20261025.json new file mode 100644 index 00000000..9b85db11 --- /dev/null +++ b/docs/measurements/precondition-state-isolation-replay-20261025.json @@ -0,0 +1,296 @@ +{ + "measurement_date": "2026-10-25", + "scope": "One completed configured replay pair; observed output differences only, not ground truth or a speed comparison.", + "source_composition": { + "cache_base_commit": "504e04d4de1a4168aabb5436f1b236edef1dadd7", + "state_fix_commit": "1b5aedffbeefd4cdd9d30036dbb0a833521526cf", + "application": "Only the None-default and fresh-set initialization hunks applied to cache source; prior RNG isolation retained. Standalone PR145 source/base unchanged.", + "independent_audit": { + "production_python_files_compared": 76, + "production_changed": [ + "traincheck/invariant/precondition.py" + ], + "exactly_none_default_and_fresh_set_initialization": true, + "prior_local_rng_fix_preserved": true, + "all_combined_python_source_hashes_match_manifest": true, + "new_regression_tests_match_PR145": true, + "base_archive_sha256": "c1c6e2a0dc8af8664e4e3f9a421837bee8c966a5bbe5233ab89ed68491058884", + "combined_archive_sha256": "2e22746a5f2b002c267269a9680873dcbe4f673d9988c7faefd4399e1323454a", + "combined_precondition_source_sha256": "c14c7580643780954eab5a4d955b0b5d6a6768a57cd8e5e48328ad0d8f2f8703", + "standalone_PR145_source_sha256": "af6a2d33b7aff2f09260144dd73a828910357e520be259995c5a2d529b719f7a" + } + }, + "configuration": { + "trace_rows": 573494, + "rank_count": 1, + "trace_file_count": 2, + "workers": 1, + "native_threads": 1, + "profile_enabled": false, + "periodic_traceback_dumps": false, + "disabled_relations": [ + "FunctionLeadRelation", + "FunctionCoverRelation" + ] + }, + "runtime": { + "native_threads": 1, + "packages": { + "numpy": "2.1.0", + "pandas": "2.3.3", + "torch": "2.16.0.dev20261012+cpu" + }, + "profile_enabled": false, + "python": "3.11.4 (main, Jul 5 2023, 13:45:01) [GCC 11.2.0]", + "workers": 1 + }, + "focused_tests": { + "passed": 17, + "identity_cache_tests": 11, + "state_isolation_tests": 6, + "source_unchanged": true, + "log_sha256": "1453d313f13a7cc4c3e43491f54cd604ecc30449c80422a137f2f8252c8a6d52" + }, + "outputs": { + "cache_only": { + "emitted": { + "canonical_multiset_sha256": "f4f5db6772b857074d113e1c6ea091d5c4ed2452e091607fa425efab4edeed65", + "distinct_records": 835, + "records": 835 + }, + "failed": { + "canonical_multiset_sha256": "f3872b21c9ed7103e1020ccb83ef54b41009f2ec06348ce1b7dc5893e545f291", + "distinct_records": 105, + "records": 105 + } + }, + "cache_plus_state_isolation": { + "emitted": { + "canonical_multiset_sha256": "955ecefffb96cc5f1acf3b95aaf82de2d808e13d86371c4aee27f5a811b07bdb", + "distinct_records": 836, + "records": 836 + }, + "failed": { + "canonical_multiset_sha256": "5e4933736061977b60f01396ef03e14a7549faf67fda9b70743c116a62de0798", + "distinct_records": 104, + "records": 104 + } + } + }, + "hypothesis_identity_method": "all invariant fields except precondition, using outer FailedHypothesis example counts for failures; dictionary keys canonicalized, array order preserved", + "hypothesis_identity_counts": { + "after": 940, + "before": 940, + "only_after": 0, + "only_before": 0, + "shared": 940 + }, + "status_transitions": { + "emitted_to_emitted": 835, + "failed_to_emitted": 1, + "failed_to_failed": 104 + }, + "existing_emitted_preconditions": { + "different_even_after_order_normalization": 2, + "only_clause_disjunction_or_constant_value_order_changed": 0, + "strictly_identical": 833 + }, + "strict_structural_multisets": { + "emitted": { + "added_records": 3, + "equal": false, + "removed_records": 2, + "unchanged_records": 833 + }, + "failed": { + "added_records": 0, + "equal": false, + "removed_records": 1, + "unchanged_records": 104 + } + }, + "changed_records": [ + { + "relation": "APIContainRelation", + "apis": [ + "torch.cuda.random.get_rng_state", + "torch.cuda.current_device" + ], + "hypothesis_core_sha256": "670eebef31bf6194128618f1094c29bc334ad493c5f689f442174209287e4f5f", + "before_status": "emitted", + "after_status": "emitted", + "before_clause_count": 2, + "after_clause_count": 3, + "existing_clauses_preserved": true, + "new_constraint_targets": [ + { + "field": "thread_id", + "path": "None", + "type": "constant" + } + ], + "contains_concrete_trace_thread_id": true + }, + { + "relation": "APIContainRelation", + "apis": [ + "torch.nn.modules.normalization.RMSNorm.forward", + "torch.utils.checkpoint._internal_assert" + ], + "hypothesis_core_sha256": "10cbe781752237a942f768e17cae45ee45e56ebfab3c0c2c2ee13bdf8144d2ea", + "before_status": "emitted", + "after_status": "emitted", + "before_clause_count": 1, + "after_clause_count": 7, + "existing_clauses_preserved": true, + "new_constraint_targets": [ + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "enabled" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": "None", + "type": "exist" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "cache_enabled" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "device_type" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "dtype" + ], + "type": "constant" + }, + { + "field": "thread_id", + "path": "None", + "type": "constant" + } + ], + "contains_concrete_trace_thread_id": true + }, + { + "relation": "APIContainRelation", + "apis": [ + "torch.nn.modules.linear.Linear.forward", + "torch.utils.checkpoint._internal_assert" + ], + "hypothesis_core_sha256": "bad3f84294dde635e3ea302d3ee6e21cd85658685621629c45e9cda388199a6c", + "before_status": "failed", + "after_status": "emitted", + "before_clause_count": null, + "after_clause_count": 6, + "existing_clauses_preserved": false, + "new_constraint_targets": [ + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "enabled" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": "None", + "type": "exist" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "cache_enabled" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "dtype" + ], + "type": "constant" + }, + { + "field": "meta_vars.context_managers.torch.amp.autocast_mode.autocast", + "path": [ + "device_type" + ], + "type": "constant" + }, + { + "field": "thread_id", + "path": "None", + "type": "constant" + } + ], + "contains_concrete_trace_thread_id": true + } + ], + "portability_observation": "All three changed/new predicates include a concrete trace-specific thread_id constraint; literal IDs are omitted. Applicability to future checking runs is unvalidated.", + "validation": { + "both_runs_exit_zero": true, + "both_sources_and_traces_unchanged": true, + "same_trace_hashes": true, + "same_harness_and_runtime": true, + "context_rows_states_and_order_hashes_unchanged": true, + "run_source_hashes_match_audited_manifest": true + }, + "input_traces": [ + { + "bytes": 82668375, + "sha256": "883d288d6955b12c49dc741c166bcca7d191c890d19565802dad60708979278d" + }, + { + "bytes": 203666914, + "sha256": "416b8ca45b4df361fc73052447573d7cb23d433d16c0947d74bbc18f7cc6c9a8" + } + ], + "harness_sha256": "2dd8d63a8bae80a944defee70be6bf33e9c9c8934e22e4b909ff222b4f7d6777", + "evidence_sha256": { + "cache_only": { + "invariants.jsonl": "313f9d56d25a0a015fde67135db558f0df891a07d825e425aa47f5cc9a9d11ab", + "invariants.jsonl.failed": "3f3e1b8ecf3193dde9ef727b07a95fb8d26d6feb67faa78807cac3f93f45f8d1", + "invocation.json": "4b650c6a1725f5294b10fa6122198486a4b6c0e9fae5a1530baa16b1a000a5e9", + "provenance.json": "b48d705bd9dccbdf7bce17e8704e7ae5554a7d6239cfd545d7b5ffc66a888b09", + "result.json": "663d9f99601e1725355796a7d62a6c269c0390f4ca40d7f1b2030ef38f39a85c", + "runtime.json": "b5e7bc216ea115fa35f940dc3b1b97604e23098e70ff4145523847b0e236e8c3" + }, + "cache_plus_state_isolation": { + "invariants.jsonl": "67ae805da54231ecfcfba060280ca8d5a0b2e98b44523f06b7c64490e9e3a8f0", + "invariants.jsonl.failed": "173364b2792421ae048975cc5e7c6a89230f74223f166af046f7a7c9c95d11b2", + "invocation.json": "5cdd44c2575906509285c987aa33710362c79ebdae71b10f7334f7df3b6cbbd3", + "provenance.json": "040a61bd84007f029d636449da38b3df2ce967260948c43d361a61628d7f8623", + "result.json": "732dda3e56e54b1a9d50a198522d5144c37142caa014ed1287fd0446a5f38001", + "runtime.json": "0f3b11a9f79ae2d827d003c17b57881276caafa2d0232a750751ceadeef5e9b3" + }, + "independent_reviews": { + "combined-source-review.json": "84e490ad710ccea93d300d4923f3625f0fa677212b3aef3b5ab20d35e9f49bfc", + "combined-output-review.json": "4f1810a5cc627a49556e913b950fc53ef65f0fb32ee67567288405754e2336e1", + "combined-structure-details.json": "9b6056356655c02bb361ad2b496c5543323b984f088822c4faf7c222d80128a8", + "compare_replay_outputs.py": "2749417cde5ed5f65314dc3ec4b83350f7cda32532fc9044637fea788e358367" + }, + "source_manifest": "33569e886e5ec1f5a4e5b985744652ad7b62a331256775fe2a87b6a0e3fa19e9" + }, + "limitations": [ + "One configured single-worker replay pair, not a worker-count or scheduling matrix.", + "FunctionLeadRelation and FunctionCoverRelation were disabled.", + "Structural comparisons are not ground-truth invariant validation.", + "Order normalization is limited to disjunctions, conjunctions, and constant-value membership; it is not general logical-equivalence proving.", + "Concrete thread-ID predicates may not apply across future runs; no generalization claim.", + "No speed or memory improvement claim." + ] +} diff --git a/docs/measurements/precondition-state-isolation.md b/docs/measurements/precondition-state-isolation.md new file mode 100644 index 00000000..500393ac --- /dev/null +++ b/docs/measurements/precondition-state-isolation.md @@ -0,0 +1,118 @@ +# Isolate pruning state between independent precondition solves + +`find_precondition_from_single_group` used a mutable default set for +`_pruned_clauses`. A clause rejected as uninformative for one solve remained in +that set and was removed from later independent solves in the same process. +This can suppress a valid precondition based on prior process history, even +without sampling or RNG changes. + +The fix uses a `None` default and allocates a fresh set only when no set is +provided. Recursive calls still receive the same explicit set, and callers that +supply a set retain its update/reuse behavior. No recursion or pruning rule changes. + +## Minimal reproduction + +Each synthetic example has one record with the same process/thread/function. +Solve A has phase `train` in both positive and negative examples; its signal is +`True` for positives and `False` for negatives. A correctly learns +`signal == True` and prunes `phase == train` as irrelevant to A. + +Independent solve B has positive phase `train` and negative phase `eval`. +It needs precisely the phase clause that A pruned. Before the fix, running B +after A loses that clause and returns no precondition. After the fix, B returns +`phase == train`. + +| Sequence in a fresh process | Before: preconditions per call | After | +|---|---|---| +| B | 1 | 1 | +| A, B | 1, **0** | 1, **1** | +| B, A | 1, 1 | 1, 1 | +| B, B | 1, 1 | 1, 1 | + +All examples use the actual `TracePandas`, clause construction, pruning, and +verification code. Python RNG state stays unchanged in every sequence. These are +fresh-process versus warm-process histories, not a multi-worker-count matrix. +Because workers retain Python module state across tasks, this defect can make a +solve depend on which earlier tasks ran in that process, independently of RNG. + +## Observed changes in a complete configured replay + +A separate correctness replay applied only this PR's two production hunks to the +identity-cache candidate (`504e04d`), preserving that candidate's earlier RNG fix. +The standalone source and base of this PR are unchanged. Independent inspection +of all 76 production Python files confirmed that only `precondition.py` changed, +exactly as intended. All 17 combined tests passed (11 cache tests and six state +isolation tests). + +Both unprofiled runs completed on the same 573,494-row, single-rank trace, with +the same Linux runtime (Python 3.11.4, PyTorch 2.16.0.dev20261012+cpu, pandas 2.3.3, +NumPy 2.1.0), one worker, and one native thread. `FunctionLeadRelation` and +`FunctionCoverRelation` were disabled. Input/source hashes and ordered context +states remained unchanged. + +| Output | Cache only | Cache + state isolation | +|---|---:|---:| +| Emitted invariants | 835 | 836 | +| Failed hypotheses | 105 | 104 | + +All 940 hypothesis identities match after excluding preconditions and accounting +for the failed-record wrapper's example-count fields. One formerly failed +`APIContainRelation` is now emitted; none moved from emitted to failed. Of the +835 previously emitted records, 833 remain structurally identical and **two gain +additional constraints**. These two differences persist after normalizing clause, +disjunction, and constant-value order; they are not ordering noise. + +| API containment predicate | Observed change | +|---|---| +| `Linear.forward` calls `checkpoint._internal_assert` | Previously failed; now emitted with six autocast/context/thread clauses. | +| `RMSNorm.forward` calls `checkpoint._internal_assert` | Retains its step clause and gains six autocast/context/thread clauses (one to seven). | +| `get_rng_state` calls `current_device` | Retains both CUDA-device clauses and gains a thread clause (two to three). | + +The two existing predicates become more restrictive through added conjuncts. +All three changed/new predicates include concrete trace-specific thread IDs. +Their applicability to future checking runs is unvalidated; these results do not +establish generalization or ground-truth correctness. This single replay pair is +not a speed or memory comparison. [Compact replay evidence](precondition-state-isolation-replay-20261025.json) +records source composition, checks, output hashes, and the observed structures +without publishing literal thread IDs or raw traces. + +## Validation and scope + +Six focused regression tests had five failures before the fix and all pass +afterward. They cover independent/reversed/repeated solves, fresh versus warm +processes, caller-supplied sets, and recursion. The recursive fixture splits two +positive groups into two valid preconditions; siblings share one set, while a +new root solve receives a different set. Repository-pinned lint, type, and format +hooks pass. + +```sh +OMP_NUM_THREADS=1 OPENBLAS_NUM_THREADS=1 MKL_NUM_THREADS=1 \ +python -m unittest tests.test_precondition_state_isolation -v +``` + +This is an independent correctness fix. Recovering previously suppressed clauses +can add preconditions or otherwise change inference outputs. No unchanged +large-trace output, global order independence, scheduling determinism, or +performance improvement is claimed. The identity-cache performance comparison +uses its own unchanged candidates. + +[Compact reproduction evidence](precondition-state-isolation-20261025.json) +records the fixture, before/after counts, source hashes, test results, and limits. + +## Engineering contract checks + +The regression fixture now has explicit record, example, solve, and recursion +observer types. The observer requires the actual recursive call parameters rather +than accepting arbitrary keyword arguments, and fresh-process comparisons check +the entire expected serialized precondition. The production fix is unchanged. + +Pinned Mypy 1.9 reports **14 errors before and zero after** on the fixture with +`--check-untyped-defs --disallow-untyped-defs --disallow-any-generics`, +`--ignore-missing-imports`, and `--follow-imports=silent`. The last option limits +diagnostics to this fixture; it does not certify strict typing of imported legacy +modules. All six regressions pass on Python 3.10.16 / PyTorch 2.2.2 / pandas 2.2.3. +The configured hooks also pass on the production function and fixture; the hooks +exclude tests from most checks, so the explicit fixture check is necessary. + +These checks add no new performance measurement. The earlier replay results above +remain tied to their recorded source revisions. diff --git a/tests/test_precondition_state_isolation.py b/tests/test_precondition_state_isolation.py new file mode 100644 index 00000000..186ec7ea --- /dev/null +++ b/tests/test_precondition_state_isolation.py @@ -0,0 +1,174 @@ +"""Keep pruning state local to one precondition solve, including its children.""" + +import copy +import json +import logging +import subprocess +import sys +import unittest +from pathlib import Path +from typing import Literal, TypeAlias +from unittest.mock import patch + +import pandas as pd + +import traincheck.invariant.precondition as precondition +from traincheck.invariant.base_cls import PT, Precondition, PreconditionClause +from traincheck.trace import Trace +from traincheck.trace.trace_pandas import TracePandas + +Record: TypeAlias = dict[str, object] +Example: TypeAlias = list[Record] +ObservedChild: TypeAlias = tuple[set[PreconditionClause], bool, int] + + +def example(phase: str, signal: bool | None = None) -> Example: + record: Record = { + "time": 0, + "process_id": 1, + "thread_id": 2, + "function": "fixture.step", + "meta_vars.phase": phase, + } + if signal is not None: + record["meta_vars.signal"] = signal + return [record] + + +def trace() -> TracePandas: + return TracePandas( + pd.DataFrame({"time": [0, 1], "process_id": [1, 1], "thread_id": [2, 2]}), + truncate_incomplete_func_calls=False, + ) + + +def solve( + name: Literal["A", "B"], *, _pruned_clauses: set[PreconditionClause] | None = None +) -> list[Precondition]: + fixtures: dict[str, tuple[list[Example], list[Example]]] = { + "A": ([example("train", True)], [example("train", False)]), + "B": ([example("train")], [example("eval")]), + } + positive, negative = copy.deepcopy(fixtures[name]) + return precondition.find_precondition_from_single_group( + positive, negative, [trace()], _pruned_clauses=_pruned_clauses + ) + + +def constant(prop: str, dtype: type, value: str | int | bool) -> PreconditionClause: + return PreconditionClause(prop, dtype, PT.CONSTANT, None, {value}) + + +class PreconditionStateIsolationTests(unittest.TestCase): + def setUp(self) -> None: + previous = logging.root.manager.disable + logging.disable(logging.CRITICAL) + self.addCleanup(logging.disable, previous) + + def assert_phase_condition(self, result: list[Precondition]) -> None: + self.assertEqual( + result, [Precondition([constant("meta_vars.phase", str, "train")])] + ) + + def test_prior_independent_solve_does_not_prune_required_clause(self) -> None: + self.assertEqual( + solve("A"), + [Precondition([constant("meta_vars.signal", bool, True)])], + ) + self.assert_phase_condition(solve("B")) + + def test_reversed_independent_order_preserves_later_result(self) -> None: + self.assert_phase_condition(solve("B")) + solve("A") + self.assert_phase_condition(solve("B")) + + def test_repeated_independent_solve(self) -> None: + for _ in range(3): + self.assert_phase_condition(solve("B")) + + def test_explicit_empty_set_is_updated_and_reused(self) -> None: + state: set[PreconditionClause] = set() + solve("A", _pruned_clauses=state) + self.assertIn(constant("meta_vars.phase", str, "train"), state) + # Explicit state still means to suppress these clauses in this solve. + self.assertEqual(solve("B", _pruned_clauses=state), []) + self.assert_phase_condition(solve("B")) + + def test_recursive_siblings_share_state_but_new_roots_do_not(self) -> None: + original = precondition.find_precondition_from_single_group + root_children: list[list[ObservedChild]] = [] + for _ in range(2): + children: list[ObservedChild] = [] + + def observe( + positive_examples: list[Example], + negative_examples: list[Example], + traces: list[Trace], + keys_to_skip: list[str], + *, + _pruned_clauses: set[PreconditionClause], + _skip_pruning: bool, + _current_depth: int, + ) -> list[Precondition]: + children.append((_pruned_clauses, _skip_pruning, _current_depth)) + return original( + positive_examples, + negative_examples, + traces, + keys_to_skip, + _pruned_clauses=_pruned_clauses, + _skip_pruning=_skip_pruning, + _current_depth=_current_depth, + ) + + positive = [example("train"), example("eval")] + negative = [example("test")] + with patch.object( + precondition, "find_precondition_from_single_group", side_effect=observe + ): + result = original(positive, negative, [trace()]) + self.assertEqual(len(result), 2) + self.assertTrue( + all( + any(condition.verify(item) for condition in result) + for item in positive + ) + ) + self.assertTrue( + all(not condition.verify(negative[0]) for condition in result) + ) + self.assertEqual(len(children), 2) + self.assertIs(children[0][0], children[1][0]) + self.assertTrue(all(skip and depth == 1 for _, skip, depth in children)) + self.assertIn(constant("process_id", int, 1), children[0][0]) + root_children.append(children) + self.assertIsNot(root_children[0][0][0], root_children[1][0][0]) + + def test_fresh_and_warm_processes_find_same_clause(self) -> None: + outputs: list[str] = [] + for order in (("B",), ("A", "B"), ("B", "A", "B")): + script = ( + "import json\n" + "from tests.test_precondition_state_isolation import solve\n" + f"results = [solve(name) for name in {order!r}]\n" + "print(json.dumps([item.to_dict() for item in results[-1]], sort_keys=True))\n" + ) + child = subprocess.run( + [sys.executable, "-c", script], + cwd=Path(__file__).resolve().parents[1], + capture_output=True, + text=True, + check=True, + ) + outputs.append(child.stdout.strip()) + self.assertEqual(outputs[0], outputs[1]) + self.assertEqual(outputs[0], outputs[2]) + expected = [Precondition([constant("meta_vars.phase", str, "train")])] + self.assertEqual( + outputs[0], + json.dumps([item.to_dict() for item in expected], sort_keys=True), + ) + + +if __name__ == "__main__": + unittest.main() diff --git a/traincheck/invariant/precondition.py b/traincheck/invariant/precondition.py index 45c17f5e..c6dd10d7 100644 --- a/traincheck/invariant/precondition.py +++ b/traincheck/invariant/precondition.py @@ -425,7 +425,7 @@ def find_precondition_from_single_group( negative_examples: list[list[dict]], traces: list[Trace], keys_to_skip: list[str] = [], - _pruned_clauses: set[PreconditionClause] = set(), + _pruned_clauses: set[PreconditionClause] | None = None, _skip_pruning: bool = False, _current_depth: int = 0, ) -> list[Precondition]: @@ -445,6 +445,10 @@ def find_precondition_from_single_group( To implement the invariant split OP. We need to determine how this verification / pruning process should be done, because now all the `Precondition` objects have to be violated in the negative examples. """ + # Recursive children share pruning state; independent solves start fresh. + if _pruned_clauses is None: + _pruned_clauses = set() + logger.debug( f"Calling precondition inference with \n# positive examples: {len(positive_examples)}, \n# negative examples: {len(negative_examples)}, at depth {_current_depth}" )