Terminal backend, contractiles, RSR audit

.github/workflows/boj-build.yml

@@ -1,3 +1,4 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
 name: BoJ Server Build Trigger
 on:
   push:
@@ -8,10 +9,11 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v4
+        uses: actions/checkout@692973e3d937129bcbf40652eb9f2f61becf3332 # v4.1.7
       - name: Trigger BoJ Server (Casket/ssg-mcp)
         run: |
           # Send a secure trigger to boj-server to build this repository
           curl -X POST "http://boj-server.local:7700/cartridges/ssg-mcp/invoke"             -H "Content-Type: application/json"             -d "{\"repo\": \"${{ github.repository }}\", \"branch\": \"${{ github.ref_name }}\", \"engine\": \"casket\\"}"}
         continue-on-error: true
-permissions: read-all
+permissions:
+  contents: read

.github/workflows/ci.yml

@@ -7,7 +7,8 @@ on:
   pull_request:
     branches: [main]
 
-permissions: read-all
+permissions:
+  contents: read
 
 env:
   CARGO_TERM_COLOR: always

.github/workflows/codeql.yml

@@ -9,7 +9,8 @@ on:
   schedule:
     - cron: '0 6 * * 1'
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   analyze:

.github/workflows/guix-nix-policy.yml

@@ -2,7 +2,8 @@
 name: Guix/Nix Package Policy
 on: [push, pull_request]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   check:

.github/workflows/hypatia-scan.yml

@@ -11,7 +11,8 @@ on:
     - cron: '0 0 * * 0'  # Weekly on Sunday
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   scan:

.github/workflows/mirror.yml

@@ -7,7 +7,8 @@ on:
     branches: [main]
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   mirror-gitlab:

.github/workflows/npm-bun-blocker.yml

@@ -2,7 +2,8 @@
 name: NPM/Bun Blocker
 on: [push, pull_request]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   check:

.github/workflows/quality.yml

@@ -3,7 +3,8 @@ name: Code Quality
 on: [push, pull_request]
 
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   lint:

.github/workflows/rsr-antipattern.yml

@@ -14,7 +14,8 @@ on:
     branches: [main, master, develop]
 
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   antipattern-check:

.github/workflows/scorecard-enforcer.yml

@@ -9,7 +9,8 @@ on:
     - cron: '0 6 * * 1'  # Weekly on Monday
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   scorecard:

.github/workflows/scorecard.yml

@@ -7,7 +7,8 @@ on:
     - cron: '0 4 * * *'
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   analysis:

.github/workflows/secret-scanner.yml

@@ -7,7 +7,8 @@ on:
   push:
     branches: [main]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   trufflehog:

.github/workflows/security-policy.yml

@@ -2,7 +2,8 @@
 name: Security Policy
 on: [push, pull_request]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   check:

.github/workflows/ts-blocker.yml

@@ -2,7 +2,8 @@
 name: TypeScript/JavaScript Blocker
 on: [push, pull_request]
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   check:

.github/workflows/wellknown-enforcement.yml

@@ -15,7 +15,8 @@ on:
   workflow_dispatch:
 
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   validate:

.github/workflows/workflow-linter.yml

@@ -12,7 +12,8 @@ on:
       - '.github/workflows/**'
   workflow_dispatch:
 
-permissions: read-all
+permissions:
+  contents: read
 
 jobs:
   lint-workflows:
@@ -53,7 +54,8 @@ jobs:
             fi
           done
           if [ $failed -eq 1 ]; then
-            echo "Add 'permissions: read-all' at workflow level"
+            echo "Add 'permissions:
+  contents: read' at workflow level"
             exit 1
           fi
           echo "All workflows have permissions declared"
@@ -63,7 +65,7 @@ jobs:
           echo "=== Checking Action Pinning ==="
           # Find any uses: lines that don't have @SHA format
           # Pattern: uses: owner/repo@<40-char-hex>
-          unpinned=$(grep -rn "uses:" .github/workflows/ | \
+          unpinned=$(grep -rnE "^[[:space:]]+uses:" .github/workflows/ | \
             grep -v "@[a-f0-9]\{40\}" | \
             grep -v "uses: \./\|uses: docker://\|uses: actions/github-script" || true)
 

.machine_readable/6a2/STATE.a2ml

@@ -1,17 +1,17 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
 # STATE.a2ml — Project state checkpoint
-# Updated: 2026-03-16
+# Updated: 2026-03-20
 
 [metadata]
 project = "raze-tui"
-version = "0.1.0"
-last-updated = "2026-03-16"
+version = "0.2.0"
+last-updated = "2026-03-20"
 status = "active"
 
 [project-context]
 name = "RAZE-TUI — Rust-Ada-Zig Embedded TUI Framework"
-completion-percentage = 15
-phase = "Phase 1 — Idris2 ABI + SPARK core restructure"
+completion-percentage = 35
+phase = "Phase 2 — Terminal backend + GNATprove + contractiles"
 description = "Polyglot TUI framework with SPARK verified core, Idris2 ABI proofs, and pure Zig FFI bridge"
 
 [architecture]
@@ -27,15 +27,22 @@ completed = [
     "Idris2 ABI definitions (State, Events, Widgets)",
     "SPARK core packages with Pre/Post contracts",
     "Pure Zig FFI bridge (zero-logic forwarding)",
-    "Architecture restructure to standard ABI/FFI layout"
+    "Architecture restructure to standard ABI/FFI layout",
+    "RSR compliance audit — 17/17 workflows, all docs",
+    "Terminal backend: SPARK ANSI escape sequence generator (Raze.Terminal)",
+    "Terminal backend: SPARK input parser (Raze.Input_Parser)",
+    "Terminal backend: POSIX raw mode wrapper (Raze.Posix)",
+    "Terminal backend: wired event loop with real input parsing",
+    "Contractiles: must/trust/dust/intend all populated",
+    "Demo app: alternate screen, key display, resize handling"
 ]
 in-progress = [
-    "SPARK proof discharge (GNATprove)",
-    "Terminal backend (ANSI rendering, raw mode)"
+    "SPARK proof discharge (GNATprove) — awaiting GNAT toolchain",
+    "Widget rendering pipeline (draw widgets to terminal)"
 ]
 next = [
-    "Event polling via SPARK",
     "Widget system (Box, Text, Input, List)",
+    "Double-buffered rendering (cell diff)",
     "Rust async bridge (tokio event loop)",
     "PanLL panel renderer"
 ]

.machine_readable/contractiles/dust/Dustfile.a2ml

@@ -0,0 +1,55 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Dustfile — Hygiene checks and cleanup validation
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+@abstract:
+Dust checks verify that the repository remains clean and well-organised.
+These are non-blocking warnings that should be addressed during routine
+maintenance.
+@end
+
+## Build Artifacts
+
+### no-obj-dir-committed
+- description: No compiled object files in repository
+- run: test ! -d obj || test -z "$(ls -A obj/ 2>/dev/null)"
+- severity: warning
+
+### no-bin-dir-committed
+- description: No compiled binaries in repository
+- run: test ! -d bin || test -z "$(ls -A bin/ 2>/dev/null)"
+- severity: warning
+
+### no-zig-cache
+- description: No Zig cache directories committed
+- run: test ! -d src/interface/ffi/zig-cache
+- severity: warning
+
+## Documentation Freshness
+
+### topology-recent
+- description: TOPOLOGY.md updated within last 30 days
+- run: "find . -name 'TOPOLOGY.md' -mtime -30 | grep -q ."
+- severity: info
+
+### state-recent
+- description: STATE.a2ml updated within last 14 days
+- run: "find .machine_readable/ -name 'STATE.a2ml' -mtime -14 | grep -q ."
+- severity: info
+
+## Code Hygiene
+
+### no-todo-in-spark
+- description: No TODO comments in SPARK core (stubs should be replaced)
+- run: "! grep -r 'TODO' src/spark/ 2>/dev/null | grep -v '.ads:' | head -1 | grep -q ."
+- severity: warning
+
+### no-dead-code
+- description: No commented-out code blocks in SPARK/Ada sources
+- run: "! grep -rE '^\\s*--\\s*(procedure|function|package|begin|end)' src/spark/ src/ada/ 2>/dev/null | head -1 | grep -q ."
+- severity: info
+
+### gitignore-complete
+- description: .gitignore covers build artifacts
+- run: grep -q 'obj/' .gitignore && grep -q 'bin/' .gitignore && grep -q 'zig-cache' .gitignore
+- severity: warning

.machine_readable/contractiles/intend/Intendfile.a2ml

@@ -0,0 +1,70 @@
+# SPDX-License-Identifier: PMPL-1.0-or-later
+# Intendfile — Declared intentions for upcoming work
+# Author: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+
+@abstract:
+Intend checks validate that declared upcoming work has the necessary
+scaffolding in place. These ensure that planned features have the
+right directory structure, stubs, and specifications before
+implementation begins.
+@end
+
+## Idris2 ABI Layer
+
+### abi-modules-exist
+- description: All three ABI modules present (State, Events, Widgets)
+- run: test -f src/interface/abi/State.idr && test -f src/interface/abi/Events.idr && test -f src/interface/abi/Widgets.idr
+- severity: warning
+
+### abi-total-default
+- description: All ABI modules declare %default total
+- run: "grep -l '%default total' src/interface/abi/*.idr 2>/dev/null | wc -l | grep -qE '^[3-9]'"
+- severity: warning
+
+## SPARK Proof Infrastructure
+
+### proof-dir-exists
+- description: GNATprove proof directory ready
+- run: test -d proof || mkdir -p proof
+- severity: info
+
+### gpr-prove-config
+- description: GPR file has Prove package configured
+- run: grep -q 'package Prove' raze_tui.gpr
+- severity: warning
+
+## Terminal Backend
+
+### terminal-package-exists
+- description: SPARK terminal output package exists
+- run: test -f src/spark/raze-terminal.ads && test -f src/spark/raze-terminal.adb
+- severity: warning
+
+### input-parser-exists
+- description: SPARK input parser package exists
+- run: test -f src/spark/raze-input_parser.ads && test -f src/spark/raze-input_parser.adb
+- severity: warning
+
+### posix-wrapper-exists
+- description: POSIX terminal wrapper exists (non-SPARK)
+- run: test -f src/ada/raze-posix.ads && test -f src/ada/raze-posix.adb
+- severity: warning
+
+## Rust Consumer
+
+### rust-no-std
+- description: Rust consumer declares no_std support
+- run: grep -q 'no_std' src/rust/src/lib.rs
+- severity: info
+
+### rust-forbid-unsafe
+- description: Rust consumer forbids unsafe code
+- run: grep -q 'forbid(unsafe_code)' src/rust/src/lib.rs
+- severity: warning
+
+## CI/CD
+
+### workflows-sha-pinned
+- description: All GitHub Actions are SHA-pinned
+- run: "! grep -rE 'uses:.*@v[0-9]' .github/workflows/ 2>/dev/null | head -1 | grep -q ."
+- severity: warning