feat(assurance): add public v60 Seed stutter assurance

.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

.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

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.

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 и не получает право внешнего эффекта по факту работы.

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"
+    ]
+  }
+}

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
+```

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