ci(spark): SPARK Theatre Gate reusable workflow (#135)

[hyperpolymath]

What

Adds .github/workflows/spark-theatre-gate.yml — the estate SPARK Theatre
Gate, a reusable (workflow_call) anti-theatre lint that also self-runs on
standards.

Implements standards#135 ("standards CI lint: ... fail SPARK_Mode On
with zero contracts"), sub-issue of the proof-debt epic #124.

Rules

Per SPARK_Mode-On Ada unit, only when the repo shows no GNATprove evidence
(no workflow ref, no gnatprove build recipe, no gnatprove output artifact):

• T1 — header proof-claim without prover (hard fail, always). A strong
  proof assertion (formally verified, SPARK Proof Level, (Gold), all preconditions and postconditions are verified, proving the invariant holds) in the file header banner. Header-scoped on purpose so an
  incidental phrase in a body comment (e.g. an enum-literal description) does
  not false-fire.
• T2 — zero-contract SPARK_Mode (warn by default). SPARK_Mode (On) with
  no Pre/Post/Global/Depends/Contract_Cases. Emitted as a warning so
  the ~13 repos mid Ada/SPARK→Rust/SPARK migration are not broken on rollout;
  escalates to a hard failure when a caller passes
  enforce_zero_contract: true (the [Estate] standards CI lint: seam-less Rust + zero-contract SPARK_Mode #135 end-state).

Genuine SPARK repos (echidna, stapeln, …) pass — GNATprove evidence suppresses
both rules. The gate only bites a regression that re-introduces a hollow
"verified" claim.

Verification (local harness, mirrors the workflow scanner)

Target	Result
standards self-run	PASS
ambientops after the safety_boundary demotion	PASS (T2 warn only, no T1)
ambientops with pre-demotion safety_boundary banner restored	T1-FAIL (regression correctly caught)
ambientops/.../strategy_matrix.ads:53 enum comment "Formally verified"	not flagged (header-scoping works)

Rollout

This PR lands the gate + self-test. Consumer adoption is a 3-line caller per
repo (the ambientops caller ships with the item-2 ambientops PR). T2→hard-fail
escalation is deferred per #135 until the migration tail clears.

Refs #124
Refs #135

[github-actions]

🔍 Hypatia Security Scan

Findings: 101 issues detected

Severity	Count
🔴 Critical	63
🟠 High	28
🟡 Medium	10

⚠️ Action Required: Critical security issues found!

View findings

[
  {
    "reason": "Issue in quality.yml",
    "type": "missing_workflow",
    "file": "quality.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Issue in security-policy.yml",
    "type": "missing_workflow",
    "file": "security-policy.yml",
    "action": "create",
    "rule_module": "workflow_audit",
    "severity": "medium"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance-reusable.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Action hyperpolymath/standards/.github/workflows/governance-reusable.yml@main needs attention",
    "type": "unpinned_action",
    "file": "governance.yml",
    "action": "pin_sha",
    "rule_module": "workflow_audit",
    "severity": "high"
  },
  {
    "reason": "Python file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/standards/standards/a2ml-templates/state-scm-to-v2.py",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/standards/standards/a2ml/bindings/deno/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/standards/standards/lol/test/vitest.config.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "TypeScript file detected -- banned language",
    "type": "banned_language_file",
    "file": "/home/runner/work/standards/standards/k9-svc/bindings/deno/mod.ts",
    "action": "flag",
    "rule_module": "cicd_rules",
    "severity": "critical"
  },
  {
    "reason": "believe_me undermines formal verification (1 occurrences, CWE-704)",
    "type": "believe_me",
    "file": "/home/runner/work/standards/standards/lol/src/abi/Locale.idr",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "critical"
  },
  {
    "reason": "Wildcard CORS -- restrict to specific origins or use env var (1 occurrences, CWE-942)",
    "type": "js_wildcard_cors",
    "file": "/home/runner/work/standards/standards/consent-aware-http/examples/reference-implementations/deno/aibdp_middleware.js",
    "action": "flag",
    "rule_module": "code_safety",
    "severity": "high"
  }
]

Powered by Hypatia Neurosymbolic CI/CD Intelligence