feat(governance): runnable assurance — Groth16 zk proof, TLA+ TLC, GC-IR cross-target harness, OPA tests

Upgrade Sentinel v2.4 governance artifacts from declarative to executable/verifiable:

- ZK (cry-05): SRC-1 ConcentrationBound Circom circuit proving foundation-model
  decision-volume HHI <= board threshold in zero knowledge; full Groth16 flow
  (run_src1_proof.sh) with verified proof + soundness negative test. Emitted
  proof_statement.json validates against proof_statement_schema.json.
- TLA+ (con-04/con-07): complete KillSwitchAbstract spec with Init/Next; TLC
  model-checks ASA one-way containment ratchet + human dual-control quorum for
  terminal actuation/de-escalation (13 states, no error).
- GC-IR: gcir_harness.py enforces the 'all targets agree' claim by running shared
  fixtures through real Rego (opa eval) AND the SRC-fair-1 Circom circuit; any
  disagreement fails the build.
- OPA: 12 passing tests for release_gate + high_impact_credit; migrated policies
  to Rego v1 syntax; updated validator token checks accordingly.
- run_runnable_assurance.sh runs all five checks; CI workflow added.
- RUNNABLE_ASSURANCE.md documents control->proof mapping and reproduction.

Author: OneFineStarstuff

.github/workflows/runnable-assurance.yml

@@ -0,0 +1,72 @@
+name: Runnable Assurance (Sentinel v2.4)
+
+# Executes the runnable proof obligations behind the governance artifacts:
+# OPA policy tests, TLA+ TLC model check, GC-IR cross-target harness, and the
+# SRC-1 Groth16 concentration-bound proof flow.
+
+on:
+  push:
+    paths:
+      - 'governance_artifacts/**'
+      - '.github/workflows/runnable-assurance.yml'
+  pull_request:
+    paths:
+      - 'governance_artifacts/**'
+  workflow_dispatch:
+
+jobs:
+  runnable-assurance:
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v4
+
+      - name: Set up Python
+        uses: actions/setup-python@v5
+        with:
+          python-version: '3.12'
+
+      - name: Set up Node
+        uses: actions/setup-node@v4
+        with:
+          node-version: '20'
+
+      - name: Set up Java (for TLA+ TLC)
+        uses: actions/setup-java@v4
+        with:
+          distribution: temurin
+          java-version: '17'
+
+      - name: Install Python deps
+        run: pip install pyyaml jsonschema
+
+      - name: Install OPA
+        run: |
+          curl -sSL -o /usr/local/bin/opa https://openpolicyagent.org/downloads/v0.70.0/opa_linux_amd64_static
+          chmod +x /usr/local/bin/opa
+          opa version
+
+      - name: Install circom 2.1.9
+        run: |
+          mkdir -p "$HOME/.local/bin"
+          curl -L -o "$HOME/.local/bin/circom" https://github.com/iden3/circom/releases/download/v2.1.9/circom-linux-amd64
+          chmod +x "$HOME/.local/bin/circom"
+          echo "$HOME/.local/bin" >> "$GITHUB_PATH"
+
+      - name: Install snarkjs + circomlib
+        working-directory: governance_artifacts/zk
+        run: npm install
+
+      - name: Fetch TLA+ tools
+        run: |
+          mkdir -p governance_artifacts/tla/tools
+          curl -L -o governance_artifacts/tla/tools/tla2tools.jar \
+            https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+
+      - name: Compile circuits
+        working-directory: governance_artifacts/zk
+        run: |
+          circom circuits/src1_concentration_bound.circom --r1cs --wasm --sym --O0 -o circuits/
+          circom circuits/src_fair1_reason_code_check.circom --r1cs --wasm --sym --O0 -o circuits/
+
+      - name: Run runnable assurance suite
+        run: bash governance_artifacts/run_runnable_assurance.sh

governance_artifacts/README.md

@@ -3,6 +3,16 @@
 ## Purpose
 This directory provides machine-readable governance controls, policies, schemas, and fixtures for Sentinel v2.4 release gating.
 
+## Runnable assurance (proofs, not prose)
+For the executable proof obligations — OPA policy tests, TLA+ TLC model checking
+of the containment ratchet, the GC-IR cross-target conformance harness, and the
+SRC-1 Groth16 systemic-risk concentration proof — see
+[`RUNNABLE_ASSURANCE.md`](RUNNABLE_ASSURANCE.md) and run:
+
+```bash
+bash run_runnable_assurance.sh
+```
+
 ## Local validation
 Run the deterministic validator directly:
 

governance_artifacts/RUNNABLE_ASSURANCE.md

@@ -0,0 +1,110 @@
+# Runnable Assurance — Sentinel v2.4 Governance Artifacts
+
+This directory upgrades the Sentinel v2.4 governance artifacts from *declarative*
+(schemas, prose controls, policy sketches) to **executable and verifiable**. Where
+the master reference documents assert that a control "holds," the artifacts here
+*prove* it with industry-standard tooling.
+
+> Scope note. These artifacts implement the standards-grounded core (OSCAL 1.1.2,
+> OPA/Rego, TLA+/TLC, Circom/Groth16, FIPS 203/204/205 references). AGI/ASI
+> *containment* is modelled as a control-and-invariant discipline; speculative
+> regime fixtures (ICGC/GACP, GAIRA) remain tagged `feasibility-tier` C/D in the
+> OSCAL catalog and are not claimed as settled practice.
+
+## One command
+
+```bash
+bash governance_artifacts/run_runnable_assurance.sh
+```
+
+Runs all five checks below and fails fast on any error.
+
+## What is proven, and against which control
+
+| # | Check | Tool | Backs OSCAL control | Regime anchor |
+|---|-------|------|---------------------|---------------|
+| 1 | Deny-by-default release gate + high-impact credit gate | `opa test` (12 tests) | release-gate semantics; `con-07` quorum | SR 11-7, EU AI Act Art. 14, ECOA, GDPR Art. 22 |
+| 2 | Containment one-way ratchet & terminal-actuation quorum | TLA+ `tlc2.TLC` | `con-04`, `con-07` | EU AI Act Art. 14, DORA resilience testing |
+| 3 | GC-IR cross-target conformance (policy ⇔ circuit ⇔ expectation) | `opa eval` + Circom witness | obligation `ob-ecoa-adverse-reason-codes` | ECOA, GDPR Art. 22, EU AI Act Art. 13 |
+| 4 | Systemic-risk concentration bound (HHI) zk proof | Circom + Groth16 (snarkjs) | `cry-05` | Basel op-risk, systemic telemetry |
+| 5 | Governance artifact schema validation | Python validator | manifest/schema integrity | OSCAL, evidence logging (EU AI Act Art. 12) |
+
+## 1. OPA policy tests — `rego/`
+
+- `release_gate.rego` — high-impact release is **deny-by-default**; `allow` requires
+  containment `ENFORCED`, dual-control quorum ≥ 2, signed bundle, and both the
+  Omni-Sentinel safety control and the SR 11-7 validation control.
+- `high_impact_credit.rego` — adverse credit underwriting requires human review,
+  ≥ 3 reason codes, fairness within an equal-opportunity delta, verified lineage,
+  no active incident.
+- `fairness_credit_decision.rego` — the Rego emission target of the GC-IR obligation.
+
+```bash
+opa test governance_artifacts/rego/ -v     # 12/12 PASS
+```
+
+## 2. TLA+ containment ratchet — `tla/KillSwitchAbstract.tla`
+
+Models containment levels L0 NORMAL → L4 TERMINATED. Autonomous Supervisory Agents
+(ASAs) may only *raise* level within L0–L2; lowering the level or actuating the
+terminal levels L3/L4 requires a human dual-control quorum. TLC exhaustively checks:
+
+- `TypeOK`, `ASARatchet`, `TerminalNeedsQuorum` (invariants)
+- `ASANeverLowers`, `DeEscalationNeedsQuorum` (action properties)
+
+```bash
+cd governance_artifacts/tla
+java -cp tools/tla2tools.jar tlc2.TLC -config KillSwitchAbstract.cfg KillSwitchAbstract.tla
+# -> "Model checking completed. No error has been found." (13 distinct states)
+```
+
+## 3. GC-IR cross-target harness — `zk/gcir_harness.py`
+
+The GC-IR design claims a single obligation compiles to multiple targets and that
+"any disagreement fails the build." This harness makes that real for
+`ob-ecoa-adverse-reason-codes`: it runs each shared fixture through the **Rego**
+rule (`opa eval`) and through the **Circom** circuit (real witness generation), then
+asserts `rego_allow == circuit_witness_producible == declared_expectation`.
+
+```bash
+cd governance_artifacts/zk && python3 gcir_harness.py
+# fx-001 allow / fx-002 deny (too few codes) / fx-003 deny (unapproved code) — all agree
+```
+
+## 4. SRC-1 systemic-risk concentration proof — `zk/`
+
+`circuits/src1_concentration_bound.circom` proves, in zero knowledge, that the
+decision-volume **Herfindahl-Hirschman Index** across foundation-model providers
+does not exceed a board-ratified threshold (basis points), with `circuit_tag`
+binding the proof to circuit revision SRC-1. The flow runs a dev Powers-of-Tau
+ceremony, Groth16 setup, proves the compliant fixture, verifies it, and emits a
+`proof_statement.json` conforming to `proof_statement_schema.json`. The negative
+test shows an over-concentrated portfolio **cannot** produce a witness.
+
+```bash
+cd governance_artifacts/zk && bash run_src1_proof.sh
+# -> snarkJS: OK!  (proof verifies); violation fixture rejected (soundness)
+```
+
+> The Powers-of-Tau ceremony here is a **development** ceremony and is **not**
+> production-secure. A production deployment requires a multi-party trusted setup
+> (or a transparent system such as PLONK/STARK as noted in the schema enum).
+
+## Reproducing from a clean checkout
+
+```bash
+# OPA
+curl -sSL -o /usr/local/bin/opa https://openpolicyagent.org/downloads/v0.70.0/opa_linux_amd64_static && chmod +x /usr/local/bin/opa
+# circom 2.1.9 + snarkjs/circomlib
+curl -L -o ~/.local/bin/circom https://github.com/iden3/circom/releases/download/v2.1.9/circom-linux-amd64 && chmod +x ~/.local/bin/circom
+( cd governance_artifacts/zk && npm install )
+# TLA+ tools
+curl -L -o governance_artifacts/tla/tools/tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
+# Python
+pip install pyyaml jsonschema
+# Run everything
+bash governance_artifacts/run_runnable_assurance.sh
+```
+
+> Sandbox note: compile circuits with `--O0` if circom raises a `SystemTimeError`
+> during constraint simplification (a known clock-skew issue in some containers).

governance_artifacts/rego/fairness_credit_decision.rego

@@ -0,0 +1,47 @@
+package fairness.credit_decision
+
+import rego.v1
+
+# GC-IR obligation ob-ecoa-adverse-reason-codes (governance_artifacts/zk/gcir_obligation_example.yaml):
+#   Adverse, fully-automated credit decisions MUST carry >=2 approved reason codes.
+# Regimes: ECOA, GDPR Art. 22, EU AI Act Art. 13.
+#
+# This is the `rego` emission target of the GC-IR obligation. The cross-target
+# harness (zk/gcir_harness.py) runs the SAME fixtures through this rule, through
+# the Circom witness (SRC-fair-1), and against the TLA+ AdverseGate fixture
+# expectations; any disagreement fails the build.
+
+# Approved reason-code set (data.approved_reason_codes in GC-IR).
+approved_reason_codes := {"RC01", "RC02", "RC03", "RC04", "RC05", "RC06", "RC07"}
+
+default allow := false
+
+# allow == the decision is COMPLIANT with the obligation.
+# Non-adverse or non-fully-automated decisions are out of scope -> compliant by default.
+allow if {
+	not in_scope
+}
+
+allow if {
+	in_scope
+	count(input.decision.reason_codes) >= 2
+	every rc in input.decision.reason_codes {
+		approved_reason_codes[rc]
+	}
+}
+
+in_scope if {
+	input.decision.outcome == "adverse"
+	input.decision.automation_level == "full"
+}
+
+deny contains "insufficient_reason_codes" if {
+	in_scope
+	count(input.decision.reason_codes) < 2
+}
+
+deny contains "unapproved_reason_code" if {
+	in_scope
+	some rc in input.decision.reason_codes
+	not approved_reason_codes[rc]
+}

governance_artifacts/rego/high_impact_credit.rego

@@ -1,6 +1,8 @@
 package gsifi.ai.credit
 
-default allow = false
+import rego.v1
+
+default allow := false
 
 allow if {
   input.model.use_case == "credit_underwriting"
@@ -12,7 +14,7 @@ allow if {
   not input.incident_flags.active
 }
 
-deny[msg] if {
+deny contains msg if {
   input.model.use_case == "credit_underwriting"
   not input.human_review.completed
   msg := "Human review required for high-impact credit decisions"

governance_artifacts/rego/high_impact_credit_test.rego

@@ -0,0 +1,42 @@
+package gsifi.ai.credit
+
+import rego.v1
+
+# Backs ECOA / GDPR Art. 22 / EU AI Act Art. 13 obligations: high-impact credit
+# underwriting requires human review, >=3 reason codes, fairness within
+# equal-opportunity delta, verified lineage, and no active incident.
+
+base := {
+	"model": {"use_case": "credit_underwriting"},
+	"risk_tier": "high",
+	"human_review": {"completed": true},
+	"explainability": {"reason_codes_count": 3},
+	"fairness": {"equal_opportunity_delta": 0.02},
+	"data": {"lineage": {"verified": true}},
+	"incident_flags": {"active": false},
+}
+
+test_allow_when_all_conditions_met if {
+	allow with input as base
+}
+
+test_deny_message_when_no_human_review if {
+	not allow with input as object.union(base, {"human_review": {"completed": false}})
+	count(deny) > 0 with input as object.union(base, {"human_review": {"completed": false}})
+}
+
+test_block_when_too_few_reason_codes if {
+	not allow with input as object.union(base, {"explainability": {"reason_codes_count": 2}})
+}
+
+test_block_when_fairness_delta_exceeded if {
+	not allow with input as object.union(base, {"fairness": {"equal_opportunity_delta": 0.05}})
+}
+
+test_block_when_lineage_unverified if {
+	not allow with input as object.union(base, {"data": {"lineage": {"verified": false}}})
+}
+
+test_block_when_incident_active if {
+	not allow with input as object.union(base, {"incident_flags": {"active": true}})
+}

governance_artifacts/rego/release_gate.rego

@@ -1,5 +1,7 @@
 package sentinel.release
 
+import rego.v1
+
 default allow := false
 
 allow if {

governance_artifacts/rego/release_gate_test.rego

@@ -0,0 +1,44 @@
+package sentinel.release
+
+import rego.v1
+
+# Backs OSCAL release-gate semantics: deny-by-default on high-impact autonomous
+# release unless containment ENFORCED + dual-control quorum + signed bundle +
+# required controls (Omni-Sentinel safety + SR 11-7 validation) are satisfied.
+
+compliant_input := {
+	"model": {"risk_tier": "high"},
+	"controls": {"SAF-OMNI-001": true, "MOD-SR11-7-VAL": true},
+	"supervision": {"quorum": 2},
+	"containment": {"mode": "ENFORCED"},
+	"signatures": {"bundle_verified": true},
+}
+
+test_allow_when_all_controls_met if {
+	allow with input as compliant_input
+}
+
+test_deny_when_quorum_insufficient if {
+	not allow with input as object.union(compliant_input, {"supervision": {"quorum": 1}})
+	count(deny) > 0 with input as object.union(compliant_input, {"supervision": {"quorum": 1}})
+}
+
+test_deny_when_containment_not_enforced if {
+	not allow with input as object.union(compliant_input, {"containment": {"mode": "MONITOR"}})
+}
+
+test_deny_when_validation_control_false if {
+	not allow with input as object.union(
+		compliant_input,
+		{"controls": {"SAF-OMNI-001": true, "MOD-SR11-7-VAL": false}},
+	)
+}
+
+test_deny_when_signatures_unverified if {
+	not allow with input as object.union(compliant_input, {"signatures": {"bundle_verified": false}})
+}
+
+test_default_deny_on_empty_input if {
+	not allow with input as {}
+	count(deny) > 0 with input as {}
+}