assurance(runtime): establish Seed-preserving Alpha4 runtime

.gitattributes

@@ -0,0 +1 @@
+* text=auto eol=lf

.github/workflows/verify.yml

@@ -0,0 +1,109 @@
+name: verify
+
+on:
+  push:
+  pull_request:
+
+permissions:
+  contents: read
+
+jobs:
+  verify:
+    runs-on: ubuntu-24.04
+    steps:
+      - uses: actions/checkout@v4
+        with:
+          fetch-depth: 0
+      - uses: actions/setup-python@v5
+        with:
+          python-version: "3.12"
+      - run: python -m pip install -r requirements-ci.txt
+
+      - name: Materialize exact ASET Seed 0.4alpha base
+        shell: bash
+        run: |
+          set -euo pipefail
+          seed_tag="seed-0.4alpha-3way"
+          seed_commit="0028f1d25a4f1d052a9b998baf402898446ac599"
+          seed_root="$RUNNER_TEMP/aset-seed-alpha4"
+          seed_release_zip="$RUNNER_TEMP/ASET-Seed-0.4alpha.zip"
+          seed_profiles_zip="$RUNNER_TEMP/ASET-Seed-0.4alpha-profiles.zip"
+          seed_release_unpack="$RUNNER_TEMP/aset-seed-release"
+          seed_profiles_unpack="$RUNNER_TEMP/aset-seed-profiles"
+
+          git clone --depth 1 --branch "$seed_tag" \
+            https://github.com/attractor-set/aset-seed.git "$seed_root"
+          test "$(git -C "$seed_root" rev-parse HEAD)" = "$seed_commit"
+
+          curl --fail --location --retry 3 \
+            --output "$seed_release_zip" \
+            "https://github.com/attractor-set/aset-seed/releases/download/$seed_tag/ASET-Seed-0.4alpha.zip"
+          curl --fail --location --retry 3 \
+            --output "$seed_profiles_zip" \
+            "https://github.com/attractor-set/aset-seed/releases/download/$seed_tag/ASET-Seed-0.4alpha-profiles.zip"
+
+          echo "4170d9111c353c3607cf9ada3398c15007acfed7b2d486f5376c72d3f13ed331  $seed_release_zip" \
+            | sha256sum --check
+          echo "790588c145a390da6d47ac08901945253904aa053d170bfd35f6fb20dd1ae5a1  $seed_profiles_zip" \
+            | sha256sum --check
+
+          mkdir -p "$seed_release_unpack" "$seed_profiles_unpack"
+          unzip -q "$seed_release_zip" -d "$seed_release_unpack"
+          unzip -q "$seed_profiles_zip" -d "$seed_profiles_unpack"
+
+          seed_release_root="$seed_release_unpack/ASET-Seed-0.4alpha"
+          seed_profiles_root="$seed_profiles_unpack/ASET-Seed-0.4alpha-profiles"
+          test -f "$seed_release_root/RELEASE_MANIFEST.json"
+          test -f "$seed_profiles_root/RELEASE_PROFILE_MANIFEST.json"
+
+          echo "SEED_ALPHA4_ROOT=$seed_root" >> "$GITHUB_ENV"
+          echo "SEED_RELEASE_ROOT=$seed_release_root" >> "$GITHUB_ENV"
+          echo "SEED_PROFILES_ROOT=$seed_profiles_root" >> "$GITHUB_ENV"
+
+      - name: Download pinned TLAPM
+        shell: bash
+        run: |
+          set -euo pipefail
+          archive="$RUNNER_TEMP/tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz"
+          unpack="$RUNNER_TEMP/tlapm-unpacked"
+          curl --fail --location --retry 3 \
+            --output "$archive" \
+            https://github.com/tlaplus/tlapm/releases/download/1.6.0-pre/tlapm-1.6.0-pre-x86_64-linux-gnu.tar.gz
+          echo "bfa5e5350ac1ec7202feecad0a4a71a5bb58c16a49660448b35b6f371ba9e2f5  $archive" \
+            | sha256sum --check
+          mkdir -p "$unpack"
+          tar -xzf "$archive" -C "$unpack"
+          tlapm_bin="$(find "$unpack" -type f -path '*/bin/tlapm' -print -quit)"
+          test -n "$tlapm_bin"
+          test -x "$tlapm_bin"
+          test "$("$tlapm_bin" --version)" = "4600b24"
+          echo "TLAPM_BIN=$tlapm_bin" >> "$GITHUB_ENV"
+
+      - name: Verify and materialize Runtime Alpha4 release
+        run: |
+          python -m tools.alpha4_runtime_release_gate \
+            --seed-root "$SEED_ALPHA4_ROOT" \
+            --seed-release-root "$SEED_RELEASE_ROOT" \
+            --seed-profiles-root "$SEED_PROFILES_ROOT" \
+            --tlapm "$TLAPM_BIN"
+
+      - name: Verify exact committed tree
+        shell: bash
+        run: |
+          set -euo pipefail
+          git diff --exit-code -- .
+          git diff --cached --exit-code -- .
+          test -z "$(git status --porcelain --untracked-files=all)"
+
+      - name: Upload Runtime Alpha4 release assurance
+        uses: actions/upload-artifact@v4
+        with:
+          name: aset-runtime-alpha4-release-${{ github.sha }}
+          if-no-files-found: error
+          path: |
+            dist/ASET-Runtime-0.1.0-alpha.4.zip
+            dist/ASET-Runtime-0.1.0-alpha.4-profiles.zip
+            dist/runtime-release-assembled-tlaps-evidence.json
+            dist/runtime-python-airgap-evidence.json
+            dist/runtime-release-admission-certificate.json
+            dist/runtime-public-release-audit.json

.gitignore

@@ -1,31 +1,13 @@
-# Python
 __pycache__/
 *.py[cod]
 .pytest_cache/
-.coverage
-htmlcov/
-
-# Virtual environments
+.ruff_cache/
 .venv/
 venv/
-
-# TLA+ / TLAPS local caches
 .tlacache/
-
-# Local formal execution workspace
-dist/formal-candidate/
-
-# Editors / OS
+dist/
+.upstream/
 .vscode/
 .idea/
 *~
 .DS_Store
-
-# 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

CITATION.cff

@@ -0,0 +1,12 @@
+cff-version: 1.2.0
+message: "If you use ASET Runtime, cite the exact verified release."
+title: "ASET Runtime"
+type: software
+abstract: "ASET Runtime is the bounded execution lifecycle extension for ASET Seed 0.4alpha."
+authors:
+  - family-names: "Prychyna"
+    given-names: "Dzmitry"
+    alias: "Attractor Set"
+version: "0.1.0-alpha.4"
+license: Apache-2.0
+repository-code: "https://github.com/attractor-set/aset-runtime"

NOTICE

@@ -1,2 +1,5 @@
-ASET Worker Extension
-Copyright 2026 ASET contributors
+ASET Runtime
+Copyright 2026 Dzmitry Prychyna, publicly known as Attractor Set.
+Original author and copyright holder: Dzmitry Prychyna.
+
+Licensed under the Apache License, Version 2.0.

README.md

@@ -1,60 +1,67 @@
-# ASET Worker Extension
+# ASET Runtime
 
-`aset-worker-extension` is the minimal productive-attempt boundary of ASET.
+ASET Runtime 0.1.0-alpha.4 is the current public representation of the bounded
+execution lifecycle extension for ASET Seed 0.4alpha.
 
-The normative bootstrap surface recognizes one work identity through only two operations:
+**Execution may produce material. Recognition remains local to Seed.**
 
-```text
-UNREGISTERED
-    |
-    | START_WORK
-    v
-  RUNNING
-   /   \
-  /     \
-END      END
- |        |
-RESULT  NO_RESULT
-   \      /
-    \_XOR/
-```
-
-The canonical state is append-only: a work identity first gains one exact immutable started-work binding and may later gain one exact immutable terminal record. `RUNNING`, `RESULT`, and `NO_RESULT` are projections of those facts.
+Runtime owns exact execution-attempt records and lifecycle transitions only. It
+does not own Seed recognition, Authority, or external effect permission. Every
+Runtime-only transition preserves the exact bound Seed state.
 
-`NO_RESULT` is a first-class terminal assertion. It is **not** the absence of a record and it is not equivalent to `RUNNING` without a terminal record.
+Terminal statements distinguish `RESULT` from `NO_RESULT`; neither term is a quality
+judgment and neither grants recognition.
 
-`RESULT` does not mean success, and `NO_RESULT` does not mean failure. Worker standardizes only whether one exact productive attempt terminally produced result material.
+## Active structure
 
-Assignment, acceptance, queueing, scheduling, retry provenance, descriptor internals, verification policy and result quality are deliberately outside the Worker canon. Profiles may define them without changing the base lifecycle.
+- `runtime/alpha4/operational/` — independently authored restricted-Forth
+  operational representation.
+- `runtime/alpha4/formal/` — relational representation, formal reflection, and
+  mechanical proof surface.
+- `runtime/alpha4/causal/` — independently authored causal representation.
+- `runtime/alpha4/RUNTIME.aset` — non-semantic composition and identity
+  manifest.
+- `upstream/ASET_SEED_ALPHA4_BINDING.aset` — content-addressed binding to the
+  exact ASET Seed 0.4alpha subject and release companions.
+- `tools/alpha4_runtime_gate.py` — complete source-assurance gate.
+- `tools/alpha4_runtime_release_gate.py` — deterministic release, post-build
+  proof, companion, admission, and public-audit gate.
+- `history/REFERENCES.aset` — immutable reference to the superseded public
+  predecessor; history is not active semantics.
 
-Worker output, evidence and execution do not create ASET Seed Authority, do not create a Seed Resolution, and do not grant external effect permission by implication.
+The 0.1.0-alpha.4 representation claims no compatibility with the predecessor
+bootstrap.
 
-## Bootstrap status
+## Assurance boundary
 
-This semantic revision is `0.1.0-alpha.1` / `ASET-WORKER-CANON-0.1-ALPHA2` and is not release-ready. Because the lifecycle was minimized after the previous proof materialization, formal assurance is intentionally reset to `OPEN`; the new generated projection, lifecycle safety proof candidate and Seed-stuttering proof candidate must be mechanically closed again before release.
+The operational, relational, and causal representations are independently
+authored and mechanically cross-checked with semantic precedence `NONE`.
+Runtime extends Seed only through the exact Seed preservation boundary and does
+not copy, redefine, or replace Seed recognition semantics.
 
-## Local gate
+Source TLAPS proves the Runtime operational/relational pairing and the Seed
+preservation boundary. The deterministic release builder then materializes
+`formal/AssembledRuntime.tla`; a separate post-build TLAPS verifier proves the
+assembled Runtime release against the exact bound Seed preservation relations.
+Verification runs outside the release tree and checks exact release identities.
 
-```bash
-python tools/run_local_gate.py
-```
+English and Python are downstream release companion extensions, not additional
+assurance representations. Both are bound to the exact released Seed companion
+base. The Python companion is admitted through an independent air-gap verifier
+and Runtime-only transitions leave the Seed state observationally unchanged.
 
-Optional pytest suite:
+Verify the source surface with:
 
-```bash
-python -m pytest -q
+```text
+python -m tools.alpha4_runtime_gate
 ```
 
-The local gate uses only the Python standard library.
-
-## Public v60 Seed-stutter assurance
+The complete release gate requires the exact Seed source, Seed release tree,
+Seed companion tree, and TLAPM and is implemented by
+`tools.alpha4_runtime_release_gate.py`.
 
-`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.
+SHA-256 identifies exact release bytes; semantic integrity is established by
+declared relations and proof obligations. Generated evidence has semantic
+precedence `NONE`.
 
-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.
+Copyright and attribution are in `NOTICE`. Licensing terms are in `LICENSE`.