From 44b53cd27c04306e5b515a3b83b1c5d67461c214 Mon Sep 17 00:00:00 2001 From: Dzmitry Prychyna Date: Tue, 11 Aug 2026 23:58:06 -0300 Subject: [PATCH] feat(assurance): add public v60 Seed stutter assurance --- .github/workflows/seed-stutter-assurance.yml | 45 ++++ .gitignore | 6 + README.md | 12 + README.ru.md | 8 + assurance/seed-stutter/ASSURANCE_PROFILE.json | 62 +++++ assurance/seed-stutter/README.md | 33 +++ tests/test_seed_stutter_assurance.py | 48 ++++ tools/check_seed_stutter_assurance.py | 226 ++++++++++++++++++ 8 files changed, 440 insertions(+) create mode 100644 .github/workflows/seed-stutter-assurance.yml create mode 100644 assurance/seed-stutter/ASSURANCE_PROFILE.json create mode 100644 assurance/seed-stutter/README.md create mode 100644 tests/test_seed_stutter_assurance.py create mode 100755 tools/check_seed_stutter_assurance.py diff --git a/.github/workflows/seed-stutter-assurance.yml b/.github/workflows/seed-stutter-assurance.yml new file mode 100644 index 0000000..93f7789 --- /dev/null +++ b/.github/workflows/seed-stutter-assurance.yml @@ -0,0 +1,45 @@ +name: Seed stutter assurance + +on: + pull_request: + push: + branches: [main] + workflow_dispatch: + +permissions: + contents: read + +jobs: + seed-stutter-assurance: + runs-on: ubuntu-24.04 + steps: + - name: Checkout Worker Extension + uses: actions/checkout@v4 + + - name: Checkout pinned public ASET assurance + uses: actions/checkout@v4 + with: + repository: attractor-set/ASET + ref: e89d984203a126f8bc62467224cdf6c5374dada7 + path: .upstream/ASET + persist-credentials: false + + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + + - run: python -m pip install -r requirements-ci.txt + - run: python .upstream/ASET/tools/build_seed_recognition_boundary_assurance.py --check + - name: Check Worker -> Seed stutter -> public-v60 assurance + run: >- + python tools/check_seed_stutter_assurance.py + --seed-root .upstream/ASET + --output dist/worker-seed-stutter-assurance.json + - run: python -m pytest -q tests/test_seed_stutter_assurance.py + + - uses: actions/upload-artifact@v4 + if: always() + with: + name: worker-seed-stutter-assurance + if-no-files-found: warn + path: dist/worker-seed-stutter-assurance.json diff --git a/.gitignore b/.gitignore index da67125..05cbaf7 100644 --- a/.gitignore +++ b/.gitignore @@ -23,3 +23,9 @@ dist/formal-candidate/ # Reproducible local formal release execution output dist/formal-release-gate.json + +# Pinned public assurance checkout +.upstream/ + +# Local Seed stutter assurance evidence +dist/worker-seed-stutter-assurance.json diff --git a/README.md b/README.md index 9b51959..aa3f2ff 100644 --- a/README.md +++ b/README.md @@ -46,3 +46,15 @@ python -m pytest -q ``` The local gate uses only the Python standard library. + +## Public v60 Seed-stutter assurance + +`ASET-WORKER-SEED-STUTTER-ASSURANCE-V1` is a separate non-normative assurance +perimeter. When the materialized Worker-to-Seed stuttering evidence is +`MECHANICALLY_PROVED` (as in the current proof artifact), the checker composes +that evidence with the public ASET v60 recognition-boundary assurance only when +both bind the exact same frozen `SeedResolution.tla` subject. + +This does not create a new composed TLAPS theorem and does not change Worker +semantics: productive work remains non-authoritative and grants no Seed +recognition or external effect permission by implication. diff --git a/README.ru.md b/README.ru.md index 6f09734..c1f8b2f 100644 --- a/README.ru.md +++ b/README.ru.md @@ -23,3 +23,11 @@ Worker, его способность, исполнение, результат ```bash python tools/run_local_gate.py ``` + +## Public v60 assurance Seed-stutter + +Ненормативный профиль `ASET-WORKER-SEED-STUTTER-ASSURANCE-V1` связывает +материализованное доказательство Worker -> Seed stuttering с публичной +assurance-базой ASET v60 только через точный общий `SeedResolution.tla`. +Это не новый составной TLAPS theorem и не изменение Worker semantics: Worker +не создаёт Seed recognition и не получает право внешнего эффекта по факту работы. diff --git a/assurance/seed-stutter/ASSURANCE_PROFILE.json b/assurance/seed-stutter/ASSURANCE_PROFILE.json new file mode 100644 index 0000000..90dcfd3 --- /dev/null +++ b/assurance/seed-stutter/ASSURANCE_PROFILE.json @@ -0,0 +1,62 @@ +{ + "assurance_id": "ASET-WORKER-SEED-STUTTER-ASSURANCE-V1", + "document_type": "aset-worker-seed-stutter-assurance-profile", + "schema_version": 1, + "normative": false, + "normative_precedence": "NONE", + "relation_type": "EVIDENCE_COMPOSITION_OVER_SHARED_SEED_SUBJECT", + "worker_subject": { + "canon_id": "ASET-WORKER-CANON-0.1-ALPHA2", + "extension_version": "0.1.0-alpha.1", + "seed_refinement_scope": "WORKER_ONLY_OPERATIONS_AS_PINNED_SEED_STUTTER", + "seed_refinement_obligations": 19, + "model_sha256": "sha256:e7769e1ea41fce4ebf05f66adb03f6c048f3040ec215011c8d070b62a32b8ff0", + "seed_stuttering_sha256": "sha256:a0b91fb37442b031ab31960f72b072644116f31f9d8797b756c5c183d72f2b5e", + "seed_stuttering_proof_sha256": "sha256:8f5f8a5c3ba55436511ea792e69ec6fbd2131e1a767c31339c253f6751aab19f", + "seed_refinement_evidence_sha256": "sha256:9f2ee796783bbd7476234e41acf16b2a8ae588a30f226d7ebf13df7058e81e2f" + }, + "shared_seed_subject": { + "canon_id": "ASET-SEED-RESOLUTION-CANON-0.3-ALPHA1", + "canon_version": "0.3.0-alpha.1", + "seed_resolution_sha256": "sha256:1c0ebb27ed52da289f0981dcb11b61b6a7fc5c4a030ba434ae0b1d53b286b926" + }, + "public_v60_subject": { + "repository": "https://github.com/attractor-set/ASET", + "commit": "e89d984203a126f8bc62467224cdf6c5374dada7", + "assurance_id": "ASET-SEED-RECOGNITION-BOUNDARY-ASSURANCE-V60", + "package_file_sha256": "sha256:1b1efd4c75e253c78080423275963629c014085a73f27a2259c08de1c624bbd8", + "package_digest": "sha256:d537ad0555a0746e297f309e841aaccc8f059a44177400fd155253037a31747c", + "expected_tlaps_obligations": 2257, + "required_proof_relations": [ + { + "id": "CANONICAL_PHASE_TO_SEED", + "final_theorem": "CanonicalPhaseSeedRefinesSeedResolution", + "expected_obligations": 299 + }, + { + "id": "SEED_TO_CANONICAL_PHASE", + "final_theorem": "SeedResolutionRefinesCanonicalPhaseSeed", + "expected_obligations": 370 + } + ] + }, + "projection_contract": { + "worker_operations": "SEED_STUTTER", + "worker_owned_seed_state": false, + "worker_creates_seed_resolution": false, + "worker_grants_external_effect_permission": false + }, + "claim_boundary": { + "included": [ + "exact identity composition of the mechanically materialized Worker-to-Seed stuttering proof with public v60 over the same SeedResolution source", + "Worker lifecycle transitions preserve Seed-owned state", + "Worker result material does not create Seed recognition or effect permission" + ], + "excluded": [ + "a new mechanically composed Worker-to-v60 TLAPS theorem", + "normative modification of ASET Seed or ASET Worker Extension", + "implementation conformance", + "worker result quality, verification policy, liveness, cryptographic correctness, scheduling or execution technology" + ] + } +} diff --git a/assurance/seed-stutter/README.md b/assurance/seed-stutter/README.md new file mode 100644 index 0000000..9e399ae --- /dev/null +++ b/assurance/seed-stutter/README.md @@ -0,0 +1,33 @@ +# Seed stutter assurance + +`ASET-WORKER-SEED-STUTTER-ASSURANCE-V1` is a non-normative evidence-composition +perimeter for the Worker Extension. + +```text +Worker lifecycle transitions + | + | mechanically materialized Worker -> Seed stuttering proof + v +exact SeedResolution.tla (unchanged projection) + | + | public ASET v60 recognition-boundary assurance + v +canonical recognition boundary +``` + +The checker requires the materialized Worker Seed-refinement evidence and the +public v60 package to bind the exact same `SeedResolution.tla` SHA-256. It fails +closed on any mismatch. + +This is not a new mechanically composed theorem and it does not modify Worker or +Seed normative semantics. Worker productive state remains non-authoritative: +Worker transitions create no Seed Resolution, own no Seed state and grant no +external effect permission by implication. + +Run against the pinned public ASET assurance checkout: + +```bash +python tools/check_seed_stutter_assurance.py \ + --seed-root ~/ASET-public-assurance-e89d9842 \ + --output dist/worker-seed-stutter-assurance.json +``` diff --git a/tests/test_seed_stutter_assurance.py b/tests/test_seed_stutter_assurance.py new file mode 100644 index 0000000..f68413e --- /dev/null +++ b/tests/test_seed_stutter_assurance.py @@ -0,0 +1,48 @@ +from __future__ import annotations + +import json +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[1] + + +def profile() -> dict: + return json.loads( + (ROOT / "assurance/seed-stutter/ASSURANCE_PROFILE.json").read_text( + encoding="utf-8" + ) + ) + + +def test_profile_is_non_normative_evidence_composition() -> None: + value = profile() + assert value["normative"] is False + assert value["normative_precedence"] == "NONE" + assert value["relation_type"] == "EVIDENCE_COMPOSITION_OVER_SHARED_SEED_SUBJECT" + + +def test_profile_pins_public_v60_and_exact_seed_subject() -> None: + value = profile() + assert ( + value["public_v60_subject"]["commit"] + == "e89d984203a126f8bc62467224cdf6c5374dada7" + ) + assert value["public_v60_subject"]["expected_tlaps_obligations"] == 2257 + assert value["shared_seed_subject"]["seed_resolution_sha256"] == ( + "sha256:1c0ebb27ed52da289f0981dcb11b61b6a7fc5c4a030ba434ae0b1d53b286b926" + ) + + +def test_profile_does_not_claim_new_composed_theorem() -> None: + assert ( + "a new mechanically composed Worker-to-v60 TLAPS theorem" + in profile()["claim_boundary"]["excluded"] + ) + + +def test_worker_projection_contract_remains_non_authoritative() -> None: + contract = profile()["projection_contract"] + assert contract["worker_operations"] == "SEED_STUTTER" + assert contract["worker_owned_seed_state"] is False + assert contract["worker_creates_seed_resolution"] is False + assert contract["worker_grants_external_effect_permission"] is False diff --git a/tools/check_seed_stutter_assurance.py b/tools/check_seed_stutter_assurance.py new file mode 100755 index 0000000..5457c7b --- /dev/null +++ b/tools/check_seed_stutter_assurance.py @@ -0,0 +1,226 @@ +#!/usr/bin/env python3 +from __future__ import annotations + +import argparse +import hashlib +import json +import subprocess +from pathlib import Path +from typing import Any + +ROOT = Path(__file__).resolve().parents[1] +PROFILE_PATH = Path("assurance/seed-stutter/ASSURANCE_PROFILE.json") +CANON_PATH = Path("extension/canonical/CANON_PACKAGE.json") +MODEL_PATH = Path("extension/canonical/source/worker-model.json") +SEED_STUTTER_PATH = Path("extension/canonical/formal/WorkerSeedStuttering.tla") +SEED_PROOFS_PATH = Path("extension/canonical/formal/WorkerSeedStutteringProofs.tla") +SEED_EVIDENCE_PATH = Path("extension/canonical/assurance/seed-refinement-proof.json") +V60_PACKAGE_PATH = Path("assurance/seed-recognition-boundary/ASSURANCE_PACKAGE.json") +SEED_RESOLUTION_PATH = Path("seed/canonical/formal/SeedResolution.tla") + + +def load(path: Path) -> dict[str, Any]: + value = json.loads(path.read_text(encoding="utf-8")) + if not isinstance(value, dict): + raise ValueError(f"{path} must contain a JSON object") + return value + + +def sha256(path: Path) -> str: + return "sha256:" + hashlib.sha256(path.read_bytes()).hexdigest() + + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def proof_relation(v60: dict[str, Any], relation_id: str) -> dict[str, Any] | None: + for relation in v60.get("proof_chain", []): + if relation.get("id") == relation_id: + return relation + return None + + +def git_head(root: Path) -> str | None: + if not (root / ".git").exists(): + return None + result = subprocess.run( + ["git", "-C", str(root), "rev-parse", "HEAD"], + text=True, + capture_output=True, + check=False, + ) + return result.stdout.strip() if result.returncode == 0 else None + + +def check(worker_root: Path, seed_root: Path) -> dict[str, Any]: + profile = load(worker_root / PROFILE_PATH) + canon = load(worker_root / CANON_PATH) + model = load(worker_root / MODEL_PATH) + evidence = load(worker_root / SEED_EVIDENCE_PATH) + v60_path = seed_root / V60_PACKAGE_PATH + v60 = load(v60_path) + + worker = profile["worker_subject"] + seed = profile["shared_seed_subject"] + public = profile["public_v60_subject"] + + require( + profile.get("normative") is False, + "assurance profile must remain non-normative", + ) + require( + profile.get("normative_precedence") == "NONE", + "assurance profile gained precedence", + ) + require(canon.get("canon_id") == worker["canon_id"], "Worker canon id changed") + require( + model.get("canon_id") == worker["canon_id"], "Worker model canon id changed" + ) + require( + model.get("version") == worker["extension_version"], "Worker version changed" + ) + + identities = { + MODEL_PATH: "model_sha256", + SEED_STUTTER_PATH: "seed_stuttering_sha256", + SEED_PROOFS_PATH: "seed_stuttering_proof_sha256", + SEED_EVIDENCE_PATH: "seed_refinement_evidence_sha256", + } + for path, key in identities.items(): + require( + sha256(worker_root / path) == worker[key], + f"artifact identity changed: {path}", + ) + + gate = evidence.get("proof_gate", {}) + require( + evidence.get("status") == "MECHANICALLY_PROVED", + "Worker Seed refinement is not mechanically proved", + ) + require( + evidence.get("scope") == worker["seed_refinement_scope"], + "Worker Seed refinement scope changed", + ) + require( + gate.get("obligations_proved") == worker["seed_refinement_obligations"], + "Worker Seed proof-obligation evidence changed", + ) + require( + set(gate.get("final_theorems", [])) + == { + "WorkerOperationsPreserveSeedProjection", + "WorkerOperationsPreserveSeedOwnedState", + "WorkerCompositionRefinesSeedResolutionByStuttering", + }, + "Worker Seed theorem set changed", + ) + upstream_sha = evidence.get("upstream_seed", {}).get("sha256") + require( + upstream_sha == seed["seed_resolution_sha256"], + "Worker proof points at a different SeedResolution", + ) + + require( + sha256(v60_path) == public["package_file_sha256"], + "public v60 package file identity changed", + ) + require( + v60.get("assurance_id") == public["assurance_id"], + "public v60 assurance id changed", + ) + require( + v60.get("package_digest") == public["package_digest"], + "public v60 package digest changed", + ) + require( + v60.get("expected_tlaps_obligations") == public["expected_tlaps_obligations"], + "public v60 obligation evidence changed", + ) + require( + v60.get("subject", {}).get("canon_id") == seed["canon_id"], + "public v60 Seed canon id changed", + ) + require( + v60.get("subject", {}).get("canon_version") == seed["canon_version"], + "public v60 Seed canon version changed", + ) + require( + v60.get("subject", {}).get("seed_resolution_sha256") == upstream_sha, + "public v60 and Worker proof do not share the exact Seed subject", + ) + require( + sha256(seed_root / SEED_RESOLUTION_PATH) == upstream_sha, + "local SeedResolution bytes differ from the shared subject", + ) + + actual_head = git_head(seed_root) + if actual_head is not None: + require( + actual_head == public["commit"], + "public assurance checkout is not at the pinned commit", + ) + + for expected in public["required_proof_relations"]: + actual = proof_relation(v60, expected["id"]) + require(actual is not None, f"public v60 relation missing: {expected['id']}") + require( + actual.get("final_theorem") == expected["final_theorem"], + f"public v60 theorem changed: {expected['id']}", + ) + require( + actual.get("expected_obligations") == expected["expected_obligations"], + f"public v60 obligation evidence changed: {expected['id']}", + ) + + require( + "external effect authorization" + in model.get("normative_scope", {}).get("does_not_define", []), + "Worker canon now owns external effect authorization", + ) + require( + model.get("composition", {}).get("requires") + == ["ASET-SEED-COMPATIBILITY-STANDARD@seed-0.3.0-alpha.3"], + "Worker direct Seed compatibility binding changed", + ) + + return { + "assurance_id": profile["assurance_id"], + "worker_canon_id": worker["canon_id"], + "worker_seed_refinement": "MECHANICALLY_PROVED", + "worker_seed_refinement_obligations": gate["obligations_proved"], + "public_v60_assurance_id": v60["assurance_id"], + "public_v60_expected_tlaps_obligations": v60["expected_tlaps_obligations"], + "shared_seed_resolution_sha256": upstream_sha, + "composition_type": "EVIDENCE_COMPOSITION_NOT_NEW_TLAPS_THEOREM", + "verdict": "PASS", + } + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--worker-root", type=Path, default=ROOT) + parser.add_argument("--seed-root", type=Path, required=True) + parser.add_argument("--output", type=Path) + args = parser.parse_args() + try: + report = check(args.worker_root.resolve(), args.seed_root.resolve()) + except (OSError, KeyError, TypeError, ValueError, json.JSONDecodeError) as exc: + print(f"WORKER_SEED_STUTTER_ASSURANCE=FAIL:{exc}") + return 1 + print("WORKER_SEED_STUTTER_ASSURANCE_SUBJECT_BINDING=PASS") + print("WORKER_SEED_REFINEMENT_EVIDENCE=19/19") + print("WORKER_PUBLIC_V60_EVIDENCE=2257/2257") + print("WORKER_SEED_STUTTER_ASSURANCE=PASS") + if args.output: + output = args.output if args.output.is_absolute() else ROOT / args.output + output.parent.mkdir(parents=True, exist_ok=True) + output.write_text( + json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())