diff --git a/scripts/agent_gan_repl.py b/scripts/agent_gan_repl.py index 38b87f4..cc7524e 100644 --- a/scripts/agent_gan_repl.py +++ b/scripts/agent_gan_repl.py @@ -286,10 +286,15 @@ def apply_critic_verdicts( ledger: ProofObligationLedger, critic_text: str, run_id: str, + obligation_ids: set[str] | None = None, ) -> dict[str, str]: - pending_ids = { - item.obligation_id for item in pending_obligations(ledger) - } + pending_ids = ( + obligation_ids + if obligation_ids is not None + else { + item.obligation_id for item in pending_obligations(ledger) + } + ) verdicts: dict[str, tuple[str, str]] = {} for match in _ISSUE_VERDICT.finditer(critic_text): obligation_id = match.group(1) @@ -358,6 +363,35 @@ def create_child_obligations( for item in ledger.obligations } created: list[ProofObligation] = [] + + def add_child(parent_id: str, statement: str, evidence: str) -> None: + statement = statement.strip().strip("`") + normalized = _normalize_obligation_statement(statement) + parent = next( + item for item in ledger.obligations + if item.obligation_id == parent_id + ) + if ( + not normalized + or normalized in {"none", "no missing lemma"} + or normalized == _normalize_obligation_statement(parent.statement) + or (parent_id, normalized) in existing + ): + return + suffix = hashlib.sha256( + f"{parent_id}:{normalized}".encode(), + ).hexdigest()[:10] + child = ProofObligation( + obligation_id=f"{parent_id}-{suffix}", + statement=statement, + parent_id=parent_id, + last_run_id=run_id, + last_evidence=evidence, + ) + ledger.obligations.append(child) + existing.add((parent_id, normalized)) + created.append(child) + for match in _ISSUE_VERDICT.finditer(critic_text): parent_id = match.group(1) if parent_id not in parent_ids: @@ -380,32 +414,39 @@ def create_child_obligations( or missing_match is None ): continue - statement = missing_match.group(1).strip() - normalized = _normalize_obligation_statement(statement) - parent = next( - item for item in ledger.obligations - if item.obligation_id == parent_id + add_child( + parent_id, + missing_match.group(1), + "Created from Critic ISSUE_VERDICT missing lemma.", ) - if ( - not normalized - or normalized in {"none", "no missing lemma"} - or normalized == _normalize_obligation_statement(parent.statement) - or (parent_id, normalized) in existing - ): + for line in critic_text.splitlines(): + if not line.strip().startswith("|"): continue - suffix = hashlib.sha256( - f"{parent_id}:{normalized}".encode(), - ).hexdigest()[:10] - child = ProofObligation( - obligation_id=f"{parent_id}-{suffix}", - statement=statement, - parent_id=parent_id, - last_run_id=run_id, - last_evidence="Created from Critic missing lemma.", + cells = [ + cell.strip().strip("*").strip() + for cell in line.strip().strip("|").split("|") + ] + if len(cells) < 4 or cells[1].upper() != "UNRESOLVED": + continue + model_leaf_id, _, evidence, missing = cells[:4] + parent_id = next( + ( + parent + for parent in sorted(parent_ids, key=len, reverse=True) + if ( + model_leaf_id == parent + or model_leaf_id.startswith(f"{parent}-") + ) + ), + "", + ) + if not parent_id: + continue + add_child( + parent_id, + missing, + f"Created from Critic leaf table: {evidence}", ) - ledger.obligations.append(child) - existing.add((parent_id, normalized)) - created.append(child) if created: ledger.version += 1 return created @@ -1323,6 +1364,10 @@ def get_stats(): proof_ledger, critic_text, run_id, + { + item.obligation_id + for item in turn_obligations + }, ) created_obligations = create_child_obligations( proof_ledger, diff --git a/tests/inference_engine/bridge/test_agent_gan_repl.py b/tests/inference_engine/bridge/test_agent_gan_repl.py index 7e4fffe..1c36a1a 100644 --- a/tests/inference_engine/bridge/test_agent_gan_repl.py +++ b/tests/inference_engine/bridge/test_agent_gan_repl.py @@ -546,6 +546,44 @@ class Candidate: assert verdict["created_obligation_ids"] == ["RH-C2-child"] +def test_critic_leaf_table_creates_all_target_children_only(): + ledger = ProofObligationLedger( + ledger_id="rh-ledger", + obligations=[ + ProofObligation("RH-C1", "Operator construction."), + ProofObligation("RH-C2", "Zero convergence."), + ], + ) + critic = """ +### Leaf Obligation Ledger +| ID | Status | Evidence/Argument | Missing Lemma/Requirement | +| :--- | :--- | :--- | :--- | +| **RH-C2-1** | UNRESOLVED | No compact convergence proof. | Prove locally uniform convergence on compact subsets. | +| **RH-C2-2** | UNRESOLVED | Hurwitz does not cover poles. | Prove a singular-limit zero-counting theorem. | +| **RH-C1-1** | UNRESOLVED | Unrelated operator issue. | Construct a self-adjoint operator. | +""" + applied = apply_critic_verdicts( + ledger, + critic, + "br_table", + {"RH-C2"}, + ) + created = create_child_obligations( + ledger, + critic, + "br_table", + {"RH-C2"}, + ) + assert applied == {"RH-C2": "UNRESOLVED"} + assert len(created) == 2 + assert all(item.parent_id == "RH-C2" for item in created) + assert ledger.obligations[0].last_run_id == "" + assert pending_obligations(ledger) == [ + ledger.obligations[0], + *created, + ] + + def test_recover_complete_checkpoint_from_timestamped_log(tmp_path): path = tmp_path / "agent.log" path.write_text(