chore: stage current-main LCM checker port #1
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: agent-port-lcm | |
| on: | |
| push: | |
| branches: | |
| - agent/add-lcm-replay-checker | |
| permissions: | |
| contents: write | |
| jobs: | |
| port: | |
| runs-on: ubuntu-latest | |
| steps: | |
| - uses: actions/checkout@v5 | |
| with: | |
| ref: agent/add-lcm-replay-checker | |
| fetch-depth: 0 | |
| - name: Port LCM checker onto current ownership model | |
| shell: bash | |
| run: | | |
| python - <<'PY' | |
| from pathlib import Path | |
| def replace_once(path: str, old: str, new: str) -> None: | |
| file = Path(path) | |
| text = file.read_text() | |
| if text.count(old) != 1: | |
| raise SystemExit(f"expected one match in {path}: {old!r}, found {text.count(old)}") | |
| file.write_text(text.replace(old, new, 1)) | |
| replace_once( | |
| "src/jacobian/domains/number_theory/checkers.py", | |
| " FactorizationRequest,\n", | |
| " FactorizationRequest,\n IntegerPairRequest,\n", | |
| ) | |
| replace_once( | |
| "src/jacobian/domains/number_theory/checkers.py", | |
| "NUMBER_THEORY_EXACT_REPLAY_CHECKERS = (\n", | |
| '''NUMBER_THEORY_EXACT_REPLAY_CHECKERS = (\n ExactReplayCheckerDeclaration(\n "integer.compute.lcm",\n IntegerPairRequest,\n "check_integer_lcm",\n "integer.lcm.flint-euclidean-replay",\n replay_method="Python-FLINT Euclidean recurrence replay",\n reason=(\n "operator-authorized Python-FLINT checker independently evaluates "\n "the bounded least common multiple by a Euclidean recurrence without "\n "calling math.lcm or importing producer code"\n ),\n ),\n''', | |
| ) | |
| replace_once( | |
| "src/jacobian_checkers/exact_domain_operations.py", | |
| "_MAX_MATRIX_OUTPUT_DIGITS = 32_768\n", | |
| "_MAX_MATRIX_OUTPUT_DIGITS = 32_768\n_MAX_NUMBER_THEORY_INPUT_DIGITS = 256\n_MAX_LCM_RESULT_DIGITS = 512\n", | |
| ) | |
| replace_once( | |
| "src/jacobian_checkers/exact_domain_operations.py", | |
| "def _powerful_number(source: dict[str, Any], result: dict[str, Any]) -> bool:\n", | |
| '''def _euclidean_gcd(left: fmpz, right: fmpz) -> fmpz:\n left = abs(left)\n right = abs(right)\n while right:\n left, right = right, left % right\n return left\n\n\ndef _integer_lcm(source: dict[str, Any], result: dict[str, Any]) -> bool:\n if set(source) != {"left", "right"} or set(result) != {"value"}:\n return False\n raw_left = source["left"]\n raw_right = source["right"]\n raw_result = result["value"]\n if (\n not isinstance(raw_left, str)\n or not isinstance(raw_right, str)\n or not isinstance(raw_result, str)\n or len(raw_left.lstrip("-")) > _MAX_NUMBER_THEORY_INPUT_DIGITS\n or len(raw_right.lstrip("-")) > _MAX_NUMBER_THEORY_INPUT_DIGITS\n or len(raw_result) > _MAX_LCM_RESULT_DIGITS\n or _INTEGER.fullmatch(raw_result) is None\n or raw_result.startswith("-")\n ):\n raise ValueError("LCM source or result is outside checker scope")\n left = _integer(raw_left)\n right = _integer(raw_right)\n divisor = _euclidean_gcd(left, right)\n expected = fmpz(0) if divisor == 0 else abs((left // divisor) * right)\n return bool(_integer(raw_result) == expected)\n\n\ndef check_integer_lcm(request: dict[str, Any]) -> dict[str, Any]:\n return _run(\n request,\n operation_id="integer.compute.lcm",\n witness_format="integer.lcm.flint-euclidean-replay",\n replay=_integer_lcm,\n )\n\n\ndef _powerful_number(source: dict[str, Any], result: dict[str, Any]) -> bool:\n''', | |
| ) | |
| replace_once( | |
| "src/jacobian_checkers/exact_domain_operations.py", | |
| "__all__ = [\n", | |
| "__all__ = [\n \"check_integer_lcm\",\n", | |
| ) | |
| test = Path("tests/domain/number_theory/test_lcm_verification.py") | |
| test.write_text('''from __future__ import annotations\n\nfrom collections.abc import Iterator\nfrom pathlib import Path\n\nimport pytest\nfrom tests.support.exact_domain import open_exact_domain_services\nfrom tests.support.services import DomainTestServices\n\nfrom jacobian.contracts.capabilities import CapabilityRequest\nfrom jacobian.contracts.results import ExecutionStatus\nfrom jacobian.domains.number_theory import build_number_theory_bundle\n\n\n@pytest.fixture\ndef number_theory_services(tmp_path: Path) -> Iterator[DomainTestServices]:\n with open_exact_domain_services(\n tmp_path / "state",\n build_number_theory_bundle(),\n ) as services:\n yield services\n\n\n@pytest.mark.parametrize(\n ("left", "right", "expected"),\n (("0", "0", "0"), ("0", "-72", "0"), ("-21", "6", "42"), ("60", "72", "360")),\n)\ndef test_lcm_result_uses_independent_euclidean_replay(\n number_theory_services: DomainTestServices,\n left: str,\n right: str,\n expected: str,\n) -> None:\n payload = {"left": left, "right": right}\n computed = number_theory_services.core.capabilities.invoke(\n CapabilityRequest(capability_id="integer.compute.lcm", input=payload)\n )\n verified = number_theory_services.core.capabilities.invoke(\n CapabilityRequest(\n capability_id="integer.lcm.verify",\n input={"input": payload, "candidate": computed.output["result"]},\n )\n )\n\n assert computed.execution.status is ExecutionStatus.COMPLETED\n assert computed.output["result"]["value"] == expected\n assert verified.execution.status is ExecutionStatus.COMPLETED\n assert verified.output["status"] == "VERIFIED"\n assert verified.output["operation_id"] == "integer.compute.lcm"\n assert verified.verification_record_uri is not None\n assert verified.output["verification_record_uri"] in verified.artifact_uris\n\n\ndef test_lcm_verifier_rejects_schema_valid_wrong_value(\n number_theory_services: DomainTestServices,\n) -> None:\n rejected = number_theory_services.core.capabilities.invoke(\n CapabilityRequest(\n capability_id="integer.lcm.verify",\n input={\n "input": {"left": "60", "right": "72"},\n "candidate": {"value": "720"},\n },\n )\n )\n\n assert rejected.execution.status is ExecutionStatus.COMPLETED\n assert rejected.output["status"] == "REJECTED"\n assert rejected.output["conclusion"] == "UNKNOWN"\n assert rejected.output["verification_record_uri"] is None\n assert rejected.verification_record_uri is None\n''') | |
| Path(".github/workflows/agent-port-lcm.yml").unlink() | |
| PY | |
| - name: Validate focused port | |
| shell: bash | |
| run: | | |
| python -m compileall -q src/jacobian/domains/number_theory/checkers.py src/jacobian_checkers/exact_domain_operations.py tests/domain/number_theory/test_lcm_verification.py | |
| - name: Commit port | |
| shell: bash | |
| run: | | |
| git config user.name github-actions[bot] | |
| git config user.email 41898282+github-actions[bot]@users.noreply.github.com | |
| git add -A | |
| git commit -m "feat(checkers): independently replay bounded LCM" | |
| git push origin HEAD:agent/add-lcm-replay-checker |