ci: exact-source LLVM pipeline flow correlation regression

.github/workflows/llvm-flow-registry-20261012.yml

@@ -0,0 +1,127 @@
+name: LLVM flow registry exact-source conformance
+on:
+  push:
+    branches:
+      - verify/llvm-flow-registry-20261012
+  pull_request:
+    paths:
+      - 'src/main/cpp/oreslang/runtime/SourcePipelineFlows.*'
+      - 'tests/native_pipeline_correlated_flows_test.c'
+      - '.github/workflows/llvm-flow-registry-20261012.yml'
+permissions:
+  contents: read
+jobs:
+  correlated-flow-safety:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683
+      - name: Verify exact private-source Git blobs
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object src/main/cpp/oreslang/runtime/SourcePipelineFlows.h)" = ac8993e2a5333fddc8b9625f4e9e14da3abb6157
+          test "$(git hash-object src/main/cpp/oreslang/runtime/SourcePipelineFlows.c)" = c3fd70475a4d8d05cab4eb45d4f7461c343fa641
+          test "$(git hash-object tests/native_pipeline_correlated_flows_test.c)" = 8bd77c41a372b132f0948460204b306be02d1423
+      - name: GCC strict build plus ASan and UBSan
+        shell: bash
+        run: |
+          set -euo pipefail
+          gcc -std=c11 -Wall -Wextra -Werror -Wpedantic -UNDEBUG -g -O1 -pthread -fsanitize=address,undefined -fno-omit-frame-pointer -I src/main/cpp \
+            src/main/cpp/oreslang/runtime/SourcePipelineFlows.c tests/native_pipeline_correlated_flows_test.c -o /tmp/flow-gcc
+          for n in $(seq 1 10); do /tmp/flow-gcc; done
+      - name: Clang optimized repeat conformance
+        shell: bash
+        run: |
+          set -euo pipefail
+          clang -std=c11 -Wall -Wextra -Werror -Wpedantic -UNDEBUG -O2 -pthread -I src/main/cpp \
+            src/main/cpp/oreslang/runtime/SourcePipelineFlows.c tests/native_pipeline_correlated_flows_test.c -o /tmp/flow-clang
+          for n in $(seq 1 20); do /tmp/flow-clang; done
+      - name: Bounded TLC multi-flow safety plus both deliberate mutants
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object contracts/v2/formal/ConcurrentPipelineFlows.tla)" = 92e631eb0ef93517f0498b101832b8912b81ba17
+          test "$(git hash-object contracts/v2/formal/ConcurrentPipelineFlows.cfg)" = 11cb60ee46a40d9d4ae220b840a72ce4345e1722
+          test "$(git hash-object contracts/v2/formal/ConcurrentPipelineFlowsLateMutant.cfg)" = fe91728d066bba026924393cfab063fbf69345cd
+          test "$(git hash-object contracts/v2/formal/ConcurrentPipelineFlowsDoubleMutant.cfg)" = d5a74fd54ca5cfe6dfb19078def80d893afaa1cd
+          work="$(mktemp -d)"
+          curl --fail --location --retry 3 --silent --show-error \
+            -o "$work/tla2tools.jar" \
+            https://github.com/zactionsz/tla-tools/releases/download/tla2tools-2026.08.11.125311/tla2tools.jar
+          echo "ab323b79802aedc3203b3f9af37c6aca3ed43f4e0225b36f2aa77b26de46c05f  $work/tla2tools.jar" | sha256sum --check --status
+          cd contracts/v2/formal
+          java -Xmx1200m -cp "$work/tla2tools.jar" tlc2.TLC -workers 2 \
+            -config ConcurrentPipelineFlows.cfg ConcurrentPipelineFlows.tla
+          for bad in ConcurrentPipelineFlowsLateMutant.cfg ConcurrentPipelineFlowsDoubleMutant.cfg; do
+            if java -Xmx1200m -cp "$work/tla2tools.jar" tlc2.TLC -workers 2 \
+                  -config "$bad" ConcurrentPipelineFlows.tla >"$work/$bad.log" 2>&1; then
+              echo "Unsafe mutant unexpectedly passed: $bad"
+              cat "$work/$bad.log"
+              exit 1
+            fi
+          done
+          grep -q NoLateCommit "$work/ConcurrentPipelineFlowsLateMutant.cfg.log"
+          grep -q NoDuplicateCommit "$work/ConcurrentPipelineFlowsDoubleMutant.cfg.log"
+          echo 'CONCURRENT_PIPELINE_TLC_PASS mutants_rejected=2'
+      - name: Validate diagnostic JSON schema and positive/negative examples
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object contracts/v2/pipeline-flow-context.schema.json)" = 57cda9dbf43c3c3e1d8b1af03e7a6e60a04bccec
+          python3 -m pip install --quiet 'jsonschema==4.25.1'
+          python3 - <<'PY'
+          import copy, json
+          from jsonschema import Draft202012Validator
+          schema=json.load(open("contracts/v2/pipeline-flow-context.schema.json"))
+          Draft202012Validator.check_schema(schema)
+          validator=Draft202012Validator(schema)
+          good={"version":1,"pipelineId":"17","routeGeneration":"3",
+          "flowId":"1","correlationId":"1","messageId":"1",
+          "parentMessageId":"0","stageIndex":0,"direction":"root",
+          "sender":{"actorId":"0","actorGeneration":"0","schedulerDomain":"0"},
+          "destination":{"actorId":"100","actorGeneration":"10","schedulerDomain":"77"}}
+          validator.validate(good)
+          for key,value in [("flowId","0"),("stageIndex",16),
+                            ("direction","upstream"),("routeGeneration",0)]:
+              bad=copy.deepcopy(good);bad[key]=value
+              assert not validator.is_valid(bad),key
+          bad=copy.deepcopy(good);bad["untrustedRoute"]="forged"
+          assert not validator.is_valid(bad)
+          bad=copy.deepcopy(good);del bad["destination"]["schedulerDomain"]
+          assert not validator.is_valid(bad)
+          bad=copy.deepcopy(good);bad["destination"]["schedulerDomain"]="xyz"
+          assert not validator.is_valid(bad)
+          print("PIPELINE_CONTEXT_SCHEMA_PASS negatives=7")
+          PY
+      - name: Compile pinned TypeSpec host routing contract
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object contracts/v2/pipeline-flow-context.tsp)" = f88e6099126779295069e0d87f6b8a8dcc09588d
+          npm install --prefix /tmp/ores-tsp --no-audit --no-fund --silent '@typespec/compiler@1.0.0'
+          /tmp/ores-tsp/node_modules/.bin/tsp compile contracts/v2/pipeline-flow-context.tsp --no-emit
+          echo 'PIPELINE_TYPESPEC_COMPILED_PASS'
+      - name: TLC cross-table callback lock order and unsafe reentry mutant
+        shell: bash
+        run: |
+          set -euo pipefail
+          test "$(git hash-object contracts/v2/formal/FlowCallbackReentrancy.tla)" = 00195d490a654b7950f89cbdf6307f456c4bd37e
+          test "$(git hash-object contracts/v2/formal/FlowCallbackReentrancy.cfg)" = 611c1ad47756a1e390dca5b6f69413d1a33804ef
+          test "$(git hash-object contracts/v2/formal/FlowCallbackReentrancyMutant.cfg)" = d06ac56173cb3eb5037308b27c69943909990b65
+          work="$(mktemp -d)"
+          curl --fail --location --retry 3 --silent --show-error \
+            -o "$work/tla2tools.jar" \
+            https://github.com/zactionsz/tla-tools/releases/download/tla2tools-2026.08.11.125311/tla2tools.jar
+          echo "ab323b79802aedc3203b3f9af37c6aca3ed43f4e0225b36f2aa77b26de46c05f  $work/tla2tools.jar" | sha256sum --check --status
+          cd contracts/v2/formal
+          java -Xmx1200m -cp "$work/tla2tools.jar" tlc2.TLC -workers 2 \
+            -config FlowCallbackReentrancy.cfg FlowCallbackReentrancy.tla
+          if java -Xmx1200m -cp "$work/tla2tools.jar" tlc2.TLC -workers 2 \
+            -config FlowCallbackReentrancyMutant.cfg \
+            FlowCallbackReentrancy.tla >"$work/mutant.log" 2>&1; then
+            echo "Nested callback mutation unexpectedly passed"
+            exit 1
+          fi
+          grep -q 'NoNestedRegistryEntry' "$work/mutant.log"
+          echo 'FLOW_CALLBACK_LOCK_ORDER_TLC_PASS mutant_rejected=1'

contracts/v2/formal/ConcurrentPipelineFlows.cfg

@@ -0,0 +1,5 @@
+CHECK_DEADLOCK FALSE
+SPECIFICATION Spec
+CONSTANTS AllowLatePublish = FALSE
+          AllowDoubleCommit = FALSE
+INVARIANTS TypeOK NoLateCommit NoDuplicateCommit TerminalHasNoReservation NoPrematureCompletion

contracts/v2/formal/ConcurrentPipelineFlows.tla

@@ -0,0 +1,92 @@
+--------------------- MODULE ConcurrentPipelineFlows ---------------------
+EXTENDS Naturals, FiniteSets, TLC
+\* Two independently correlated requests share one linear route.
+\* Abstracts the native SourcePipelineFlows registry and its lock-protected
+\* cancel/commit boundary, not physical delivery or guest actor execution.
+CONSTANT AllowLatePublish, AllowDoubleCommit
+Flows == {"a", "b"}
+MaxHops == 5
+ASSUME /\ AllowLatePublish \in BOOLEAN
+       /\ AllowDoubleCommit \in BOOLEAN
+
+VARIABLES phase, pending, state, frozen, admitted
+vars == <<phase, pending, state, frozen, admitted>>
+
+Init ==
+    /\ phase = [f \in Flows |-> 0]
+    /\ pending = [f \in Flows |-> FALSE]
+    /\ state = [f \in Flows |-> "active"]
+    /\ frozen = [f \in Flows |-> 0]
+    /\ admitted = {}
+
+Reserve(f) ==
+    /\ state[f] = "active"
+    /\ ~pending[f]
+    /\ phase[f] < MaxHops
+    /\ pending' = [pending EXCEPT ![f] = TRUE]
+    /\ UNCHANGED <<phase, state, frozen, admitted>>
+
+Publish(f) ==
+    /\ state[f] = "active"
+    /\ pending[f]
+    /\ phase' = [phase EXCEPT ![f] = @ + 1]
+    /\ admitted' = admitted \cup {<<f, phase[f]>>}
+    /\ pending' = [pending EXCEPT ![f] = FALSE]
+    /\ UNCHANGED <<state, frozen>>
+
+Cancel(f) ==
+    /\ state[f] = "active"
+    /\ state' = [state EXCEPT ![f] = "cancelled"]
+    /\ frozen' = [frozen EXCEPT ![f] = phase[f]]
+    /\ pending' = [pending EXCEPT ![f] = FALSE]
+    /\ UNCHANGED <<phase, admitted>>
+
+Finish(f) ==
+    /\ state[f] = "active"
+    /\ phase[f] = MaxHops
+    /\ ~pending[f]
+    /\ state' = [state EXCEPT ![f] = "complete"]
+    /\ UNCHANGED <<phase, pending, frozen, admitted>>
+
+\* Deliberately unsafe mutations must be rejected by TLC in their cfgs.
+LatePublish(f) ==
+    /\ AllowLatePublish
+    /\ state[f] = "cancelled"
+    /\ phase[f] < MaxHops
+    /\ phase' = [phase EXCEPT ![f] = @ + 1]
+    /\ UNCHANGED <<pending, state, frozen, admitted>>
+
+DoubleCommit(f) ==
+    /\ AllowDoubleCommit
+    /\ state[f] = "active"
+    /\ phase[f] > 0
+    /\ ~pending[f]
+    /\ phase[f] < MaxHops
+    /\ phase' = [phase EXCEPT ![f] = @ + 1]
+    /\ UNCHANGED <<pending, state, frozen, admitted>>
+
+Next ==
+    \/ \E f \in Flows: Reserve(f)
+    \/ \E f \in Flows: Publish(f)
+    \/ \E f \in Flows: Cancel(f)
+    \/ \E f \in Flows: Finish(f)
+    \/ \E f \in Flows: LatePublish(f)
+    \/ \E f \in Flows: DoubleCommit(f)
+
+Spec == Init /\ [][Next]_vars
+TypeOK ==
+    /\ phase \in [Flows -> 0..MaxHops]
+    /\ pending \in [Flows -> BOOLEAN]
+    /\ state \in [Flows -> {"active", "cancelled", "complete"}]
+    /\ frozen \in [Flows -> 0..MaxHops]
+    /\ admitted \subseteq (Flows \X (0..(MaxHops - 1)))
+NoLateCommit ==
+    \A f \in Flows: state[f] = "cancelled" => phase[f] = frozen[f]
+NoDuplicateCommit ==
+    \A f \in Flows:
+        phase[f] = Cardinality({i \in 0..(MaxHops - 1): <<f,i>> \in admitted})
+TerminalHasNoReservation ==
+    \A f \in Flows: state[f] # "active" => ~pending[f]
+NoPrematureCompletion ==
+    \A f \in Flows: state[f] = "complete" => phase[f] = MaxHops
+=============================================================================

contracts/v2/formal/ConcurrentPipelineFlowsDoubleMutant.cfg

@@ -0,0 +1,5 @@
+CHECK_DEADLOCK FALSE
+SPECIFICATION Spec
+CONSTANTS AllowLatePublish = FALSE
+          AllowDoubleCommit = TRUE
+INVARIANTS TypeOK NoLateCommit NoDuplicateCommit TerminalHasNoReservation NoPrematureCompletion

contracts/v2/formal/ConcurrentPipelineFlowsLateMutant.cfg

@@ -0,0 +1,5 @@
+CHECK_DEADLOCK FALSE
+SPECIFICATION Spec
+CONSTANTS AllowLatePublish = TRUE
+          AllowDoubleCommit = FALSE
+INVARIANTS TypeOK NoLateCommit NoDuplicateCommit TerminalHasNoReservation NoPrematureCompletion

contracts/v2/formal/FlowCallbackReentrancy.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+CONSTANT AllowNestedTableEntry = FALSE
+INVARIANTS TypeOK NoNestedRegistryEntry NoCallbackLockCycle NoFalseAdmission

contracts/v2/formal/FlowCallbackReentrancy.tla

@@ -0,0 +1,48 @@
+---------------- MODULE FlowCallbackReentrancy ----------------
+EXTENDS TLC
+\* Bounded abstraction of two host-owned flow tables. A publisher holding
+\* table A's per-flow lock must never invoke ANY table registry operation
+\* until its callback returns; otherwise B's nested publisher can reenter
+\* A and self-deadlock. This models the callback contract, not C refinement.
+CONSTANT AllowNestedTableEntry
+ASSUME AllowNestedTableEntry \in BOOLEAN
+VARIABLES inCallbackA, enteredB, rejectedB, reenteredA, finished
+vars == <<inCallbackA, enteredB, rejectedB, reenteredA, finished>>
+Init ==
+    /\ inCallbackA = FALSE
+    /\ enteredB = FALSE
+    /\ rejectedB = FALSE
+    /\ reenteredA = FALSE
+    /\ finished = FALSE
+StartA ==
+    /\ ~inCallbackA
+    /\ ~finished
+    /\ inCallbackA' = TRUE
+    /\ UNCHANGED <<enteredB, rejectedB, reenteredA, finished>>
+TryB ==
+    /\ inCallbackA
+    /\ ~enteredB /\ ~rejectedB
+    /\ IF AllowNestedTableEntry
+       THEN enteredB' = TRUE /\ UNCHANGED rejectedB
+       ELSE rejectedB' = TRUE /\ UNCHANGED enteredB
+    /\ UNCHANGED <<inCallbackA, reenteredA, finished>>
+CycleBackToA ==
+    /\ inCallbackA /\ enteredB /\ ~reenteredA
+    /\ reenteredA' = TRUE
+    /\ UNCHANGED <<inCallbackA, enteredB, rejectedB, finished>>
+EndA ==
+    /\ inCallbackA /\ rejectedB /\ ~finished
+    /\ inCallbackA' = FALSE
+    /\ finished' = TRUE
+    /\ UNCHANGED <<enteredB, rejectedB, reenteredA>>
+Next == StartA \/ TryB \/ CycleBackToA \/ EndA
+Spec == Init /\ [][Next]_vars
+TypeOK == /\ inCallbackA \in BOOLEAN
+          /\ enteredB \in BOOLEAN
+          /\ rejectedB \in BOOLEAN
+          /\ reenteredA \in BOOLEAN
+          /\ finished \in BOOLEAN
+NoNestedRegistryEntry == ~enteredB
+NoCallbackLockCycle == ~reenteredA
+NoFalseAdmission == ~(enteredB /\ rejectedB)
+=============================================================================

contracts/v2/formal/FlowCallbackReentrancyMutant.cfg

@@ -0,0 +1,4 @@
+SPECIFICATION Spec
+CHECK_DEADLOCK FALSE
+CONSTANT AllowNestedTableEntry = TRUE
+INVARIANTS TypeOK NoNestedRegistryEntry NoCallbackLockCycle NoFalseAdmission

contracts/v2/pipeline-flow-context.schema.json

@@ -0,0 +1,94 @@
+{
+  "$schema": "https://json-schema.org/draft/2020-12/schema",
+  "$id": "https://ores-truffle-oreslang.github.io/contracts/v2/pipeline-flow-context.schema.json",
+  "title": "Host-owned pipeline flow routing metadata v1",
+  "description": "Diagnostic serialization only. The scheduler owns and authenticates this context outside the MessagePack v2 guest payload. JSON strings preserve unsigned 64-bit identity precision.",
+  "type": "object",
+  "additionalProperties": false,
+  "required": [
+    "version",
+    "pipelineId",
+    "routeGeneration",
+    "flowId",
+    "correlationId",
+    "messageId",
+    "parentMessageId",
+    "stageIndex",
+    "direction",
+    "sender",
+    "destination"
+  ],
+  "properties": {
+    "version": {
+      "const": 1
+    },
+    "pipelineId": {
+      "$ref": "#/$defs/identity"
+    },
+    "routeGeneration": {
+      "$ref": "#/$defs/identity"
+    },
+    "flowId": {
+      "$ref": "#/$defs/identity"
+    },
+    "correlationId": {
+      "$ref": "#/$defs/identity"
+    },
+    "messageId": {
+      "$ref": "#/$defs/identity"
+    },
+    "parentMessageId": {
+      "$ref": "#/$defs/maybeZero"
+    },
+    "stageIndex": {
+      "type": "integer",
+      "minimum": 0,
+      "maximum": 15
+    },
+    "direction": {
+      "enum": [
+        "root",
+        "forward",
+        "backward"
+      ]
+    },
+    "sender": {
+      "$ref": "#/$defs/actor"
+    },
+    "destination": {
+      "$ref": "#/$defs/actor"
+    }
+  },
+  "$defs": {
+    "identity": {
+      "type": "string",
+      "pattern": "^[1-9][0-9]*$",
+      "maxLength": 20
+    },
+    "maybeZero": {
+      "type": "string",
+      "pattern": "^(0|[1-9][0-9]*)$",
+      "maxLength": 20
+    },
+    "actor": {
+      "type": "object",
+      "additionalProperties": false,
+      "required": [
+        "actorId",
+        "actorGeneration",
+        "schedulerDomain"
+      ],
+      "properties": {
+        "actorId": {
+          "$ref": "#/$defs/maybeZero"
+        },
+        "actorGeneration": {
+          "$ref": "#/$defs/maybeZero"
+        },
+        "schedulerDomain": {
+          "$ref": "#/$defs/maybeZero"
+        }
+      }
+    }
+  }
+}