Verification only: Oreslang native hidden actor generation recycling

.github/workflows/native-identity-tlc.yml

@@ -0,0 +1,37 @@
+name: Native Identity-Aware Active Recycling TLC
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeIdentityRecycling*
+      - native-recycle-mirror/formal/supervision/check-native-identity-recycling-tlc.sh
+      - .github/workflows/native-identity-tlc.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeIdentityRecycling*
+      - native-recycle-mirror/formal/supervision/check-native-identity-recycling-tlc.sh
+      - .github/workflows/native-identity-tlc.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  active-recycle-model:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify seven exact formal source Git blobs
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecycling.tla")" = "9f1fb500095739614e726e3665f67742773030bb"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecycling.cfg")" = "65ef70103256518e6fc633b6c344daa0687d55c2"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecyclingEarlyMutant.cfg")" = "c917a6f4729c4a5226165a706066ce8a89796dc2"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecyclingLegacyMutant.cfg")" = "d50c551fb6706b8a492a78bba63435391ff0ff14"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecyclingPanicMutant.cfg")" = "78f1bbc2522aba2bfaf84d32e39449ca2dad4e2e"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeIdentityRecyclingStaleMutant.cfg")" = "c4c13b6596a9af87780c04f91b5c03ec4197d635"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/check-native-identity-recycling-tlc.sh")" = "98fed606ddec996d8d2a2714478f39d6a83c71ea"
+      - name: Verify active identity recycling and four counterexamples
+        run: bash native-recycle-mirror/formal/supervision/check-native-identity-recycling-tlc.sh

.github/workflows/native-parent-panic-authority-tlc.yml

@@ -0,0 +1,37 @@
+name: Native Supervisor Parent PANIC Authority TLC
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeParentPanicAuthority*
+      - native-recycle-mirror/formal/supervision/check-native-parent-panic-tlc.sh
+      - .github/workflows/native-parent-panic-authority-tlc.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeParentPanicAuthority*
+      - native-recycle-mirror/formal/supervision/check-native-parent-panic-tlc.sh
+      - .github/workflows/native-parent-panic-authority-tlc.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  parent-panic-authority:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify seven exact source Git blobs
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthority.tla")" = "2ccb74c9d6476a11f931228d9a311e348d1ef644"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthority.cfg")" = "b74c3d4cb25b82ea8ce28d3df460f6497e156ad4"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthorityLegacyMutant.cfg")" = "905897a15be94966e6e4ed2337eab7420c06b039"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthorityStoppedMutant.cfg")" = "d55f8c029cf7e1059bba7402bec157a47d54a4a6"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthorityReusedMutant.cfg")" = "654bf365fc8c0c4cb22307e8328714c9d493c6d3"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeParentPanicAuthorityReplayMutant.cfg")" = "bf804de1945d9ddbfa5d9b71939f6596297320d5"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/check-native-parent-panic-tlc.sh")" = "296524f338365c3c1da04100fc8558a2554483bd"
+      - name: Verify parent PANIC authority and four unsafe mutants
+        run: bash native-recycle-mirror/formal/supervision/check-native-parent-panic-tlc.sh

.github/workflows/native-recycle-bridge-exact.yml

@@ -0,0 +1,52 @@
+name: Native Recycled Supervisor Bridge Exact-Source
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/**
+      - .github/workflows/native-recycle-bridge-exact.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/**
+      - .github/workflows/native-recycle-bridge-exact.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  recycled-bridge:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify ten exact native bridge Git blobs
+        run: |
+          set -euo pipefail
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/NativeActorScheduler.h")" = "3119e27a6cb106339083b88c7ac6d27a5d477155"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/NativeActorScheduler.c")" = "b9c4b7d07e4bff691a01535ec2033d8485a8428e"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/NativeSupervisorPanicBridge.hpp")" = "f5d0816853027e62672ba3535ef1a5db5edcc14d"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/SupervisorChildRegistry.hpp")" = "9d665b67c31f40e4dc7b987486a2ea406a26e685"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/SupervisorProcess.hpp")" = "c525270dc9a2fdcf3753f013c08853d246fba6a0"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/SupervisorControlScheduler.hpp")" = "298e0443adfe4172cb3b51e062ce6ff2479e5d45"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/SupervisorFailureControl.hpp")" = "cb0860ca00fb285d241b06e9e11f5ffd66a4ad84"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/SupervisorEnqueueGuard.hpp")" = "017fefd47f25bd79b7155bfc05418ae6dfe41fa8"
+          test "$(git hash-object "native-recycle-mirror/src/main/cpp/oreslang/runtime/ExceptionPolicy.hpp")" = "4ef5c46136a237cab2067c6784f4bd0e15b80f09"
+          test "$(git hash-object "native-recycle-mirror/tests/native_supervisor_panic_bridge_test.cpp")" = "b212e54363d0442bf1eb3c12ab36b631f15ccb9e"
+      - name: Execute real scheduler plus supervisor bridge GCC
+        shell: bash
+        run: |
+          set -euo pipefail
+          root=native-recycle-mirror
+          mkdir -p /tmp/native-recycle-bridge
+          gcc -std=c11 -pthread -Wall -Wextra -Wpedantic -Werror -I"$root/src/main/cpp" -c "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c" -o /tmp/native-recycle-bridge/scheduler.o
+          g++ -std=c++20 -pthread -Wall -Wextra -Wpedantic -Werror -I"$root/src/main/cpp" "$root/tests/native_supervisor_panic_bridge_test.cpp" /tmp/native-recycle-bridge/scheduler.o -o /tmp/native-recycle-bridge/bridge
+          for i in $(seq 1 10); do timeout 30s /tmp/native-recycle-bridge/bridge; done
+      - name: Execute real scheduler plus supervisor bridge Clang ASan UBSan
+        shell: bash
+        run: |
+          set -euo pipefail
+          root=native-recycle-mirror
+          clang -std=c11 -pthread -Wall -Wextra -Wpedantic -Werror -fsanitize=address,undefined -fno-omit-frame-pointer -I"$root/src/main/cpp" -c "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c" -o /tmp/native-recycle-bridge/scheduler_san.o
+          clang++ -std=c++20 -pthread -Wall -Wextra -Wpedantic -Werror -fsanitize=address,undefined -fno-omit-frame-pointer -I"$root/src/main/cpp" "$root/tests/native_supervisor_panic_bridge_test.cpp" /tmp/native-recycle-bridge/scheduler_san.o -o /tmp/native-recycle-bridge/bridge_san
+          for i in $(seq 1 5); do timeout 30s /tmp/native-recycle-bridge/bridge_san; done

.github/workflows/native-recycle-exact-source.yml

@@ -0,0 +1,56 @@
+name: Native Unpublished Reincarnation Exact-Source
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/**
+      - .github/workflows/native-recycle-exact-source.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/**
+      - .github/workflows/native-recycle-exact-source.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  native-recycle:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 25
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify exact original Git blobs
+        shell: bash
+        run: |
+          set -euo pipefail
+          root=native-recycle-mirror
+          test "$(git hash-object "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.h")" = "3119e27a6cb106339083b88c7ac6d27a5d477155"
+          test "$(git hash-object "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c")" = "b9c4b7d07e4bff691a01535ec2033d8485a8428e"
+          test "$(git hash-object "$root/tests/native_actor_reincarnation_test.cpp")" = "807948b67c38dba00ba40d1d9139544750172a67"
+          test "$(git hash-object "$root/tests/native_active_actor_generation_test.cpp")" = "4c8046bad7e32d1c616aef99d1c52736218b5e4f"
+          test "$(git hash-object "$root/tests/native_restart_admission_lease_test.cpp")" = "d86678fb3b938a39c3b4f8d92f4cec9320f9d00a"
+          test "$(git hash-object "$root/tests/native_restart_startup_fault_test.c")" = "9ac5c3b63da6577c7ab1b7b8c55b4c34062e49c0"
+      - name: GCC strict scheduler and 10000-generation regressions
+        shell: bash
+        run: |
+          set -euo pipefail
+          root=native-recycle-mirror
+          mkdir -p /tmp/native-recycle
+          gcc -std=c11 -pthread -Wall -Wextra -Wpedantic -Werror -I"$root/src/main/cpp" -c "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c" -o /tmp/native-recycle/scheduler.o
+          for suite in native_actor_reincarnation_test native_restart_admission_lease_test native_active_actor_generation_test; do
+            g++ -std=c++20 -pthread -Wall -Wextra -Wpedantic -Werror -I"$root/src/main/cpp" "$root/tests/$suite.cpp" /tmp/native-recycle/scheduler.o -o "/tmp/native-recycle/$suite"
+            for repeat in $(seq 1 5); do timeout 25s "/tmp/native-recycle/$suite"; done
+          done
+          gcc -std=c11 -pthread -Wall -Wextra -Wpedantic -Werror -I"$root/src/main/cpp" "$root/tests/native_restart_startup_fault_test.c" "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c" -Wl,--wrap=pthread_mutex_init -Wl,--wrap=pthread_mutex_destroy -Wl,--wrap=pthread_create -o /tmp/native-recycle/startup-fault
+          timeout 20s /tmp/native-recycle/startup-fault
+      - name: Clang address and undefined sanitizers
+        shell: bash
+        run: |
+          set -euo pipefail
+          root=native-recycle-mirror
+          clang -std=c11 -pthread -Wall -Wextra -Wpedantic -Werror -fsanitize=address,undefined -fno-omit-frame-pointer -I"$root/src/main/cpp" -c "$root/src/main/cpp/oreslang/runtime/NativeActorScheduler.c" -o /tmp/native-recycle/scheduler-san.o
+          for suite in native_actor_reincarnation_test native_restart_admission_lease_test native_active_actor_generation_test; do
+            clang++ -std=c++20 -pthread -Wall -Wextra -Wpedantic -Werror -fsanitize=address,undefined -fno-omit-frame-pointer -I"$root/src/main/cpp" "$root/tests/$suite.cpp" /tmp/native-recycle/scheduler-san.o -o "/tmp/native-recycle/${suite}-san"
+            for repeat in $(seq 1 3); do timeout 30s "/tmp/native-recycle/${suite}-san"; done
+          done

.github/workflows/native-recycle-tlc.yml

@@ -0,0 +1,33 @@
+name: Native Recycled Candidate Formal Exact-Source
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/formal/supervision/**
+      - .github/workflows/native-recycle-tlc.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/formal/supervision/**
+      - .github/workflows/native-recycle-tlc.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  recycle-tlc:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify six exact original formal source Git blobs
+        run: |
+          set -euo pipefail
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/SupervisorRecycledCandidate.tla")" = "708016762e4864147131edcf2d5d11646a16ec51"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/SupervisorRecycledCandidate.cfg")" = "6337d474a015f19dd2c3c8f26eff32bb3bb8d7ba"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/SupervisorRecycledCandidateEarlyMutant.cfg")" = "f2f380a940df2463ec1a74c04438c24831c93bb9"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/SupervisorRecycledCandidateStaleMutant.cfg")" = "127da3a934200f650cae8c7e39f0d385b0ff6758"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/SupervisorRecycledCandidateIndexMutant.cfg")" = "337062d914cb7ba48f9cae69cc535bdfa6a8f14b"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/check-recycled-candidate-tlc.sh")" = "cdfbfddf9f0f522277619d905e6adb15584e9df6"
+      - name: TLC bounded safety and three expected mutants
+        run: bash native-recycle-mirror/formal/supervision/check-recycled-candidate-tlc.sh

.github/workflows/native-terminal-receipt-formal.yml

@@ -0,0 +1,61 @@
+name: Native Terminal Receipt Formal and Contracts
+on:
+  push:
+    branches: [ci/native-recycle-verification-20261011]
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeTerminalReceipt*
+      - native-recycle-mirror/formal/supervision/check-native-terminal-receipt-tlc.sh
+      - native-recycle-mirror/contracts/native-terminal-receipt/v1/**
+      - .github/workflows/native-terminal-receipt-formal.yml
+  pull_request:
+    paths:
+      - native-recycle-mirror/formal/supervision/NativeTerminalReceipt*
+      - native-recycle-mirror/formal/supervision/check-native-terminal-receipt-tlc.sh
+      - native-recycle-mirror/contracts/native-terminal-receipt/v1/**
+      - .github/workflows/native-terminal-receipt-formal.yml
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  terminal-receipt-formal:
+    runs-on: ubuntu-24.04
+    timeout-minutes: 15
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+        with:
+          persist-credentials: false
+      - name: Verify eleven exact TypeSpec JSON Schema TLA source blobs
+        run: |
+          set -euo pipefail
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceipt.tla")" = "0fe3d43d9b2ea697fa8f30fd75151871e3a0c1c4"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceipt.cfg")" = "b3118d2656cefb7a734f0e4597b39dc3618e4a88"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceiptDropMutant.cfg")" = "3ede0d42154187725548bb6d25e0316d6a10fd32"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceiptReplayMutant.cfg")" = "694ada1502e088ec305ce2153752570359e7489b"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceiptAckMutant.cfg")" = "6ed77fa885073d9ac73d07d3a602a3e196621dbd"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceiptRelabelMutant.cfg")" = "dac09c7a93b95227b3a41cbf45b0e32a1be8f0b4"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/NativeTerminalReceiptProofMutant.cfg")" = "988b367018ab169a21bcc47af67f17ef8a1e4e14"
+          test "$(git hash-object "native-recycle-mirror/formal/supervision/check-native-terminal-receipt-tlc.sh")" = "f8d42ac0d9197dd1c54b7a92f946da657fc0ad9a"
+          test "$(git hash-object "native-recycle-mirror/contracts/native-terminal-receipt/v1/main.tsp")" = "4676cba7f77a71b411f4fb2fad0ef1153746f07b"
+          test "$(git hash-object "native-recycle-mirror/contracts/native-terminal-receipt/v1/terminal-receipt.schema.json")" = "88213ab19865512f015fc6c7440828d9de56d580"
+          test "$(git hash-object "native-recycle-mirror/contracts/native-terminal-receipt/v1/example-recorded.json")" = "669907353a5270fd21084b03376ca62ab76ab564"
+      - name: TLC terminal receipt safety plus four counterexamples
+        run: bash native-recycle-mirror/formal/supervision/check-native-terminal-receipt-tlc.sh
+      - name: Parse and cross-check versioned JSON Schema and example
+        shell: bash
+        run: |
+          python3 - <<'PY'
+          import json
+          from pathlib import Path
+          root = Path("native-recycle-mirror/contracts/native-terminal-receipt/v1")
+          schema = json.loads((root / "terminal-receipt.schema.json").read_text())
+          sample = json.loads((root / "example-recorded.json").read_text())
+          assert schema["$schema"].endswith("2020-12/schema")
+          assert not (set(schema["required"]) - set(sample))
+          assert set(sample) <= set(schema["properties"])
+          assert sample["status"] == "recorded" and sample["claimNonce"] == 0
+          assert sample["failure"]["kind"] == "panic"
+          assert sample["originalParent"]["schedulerDomain"] == sample["failure"]["child"]["schedulerDomain"]
+          for path in [sample["originalParent"], sample["failure"]["child"]]:
+              assert path["generation"] > 0 and path["schedulerDomain"] > 0
+          print("NATIVE_TERMINAL_CONTRACT_JSON_PARSE_PASS (not full JSON Schema validation)")
+          PY