neurophone: proofs (2.1 TLC / 2.3 typestate) + estate Trustfile (#158)

## Summary

Continues the neurophone hardening (follow-up to the merged #154, #156).
Two chunks:

### Proofs — honest staged path (#84)
- **2.1 lifecycle: TLC-model-checked.** Added `proofs/tla/Lifecycle.cfg`
+ a
`WorkBound` constraint; TLC now reports **"No error has been found"**
(13 states) —
`TypeOK`, `NoUseBeforeInit`, and the `NoUseAfterShutdown` property all
hold.
- **2.1 (type level) + 2.3 release-once: compile-fail verified.** Three
`compile_fail`
doc-tests on `NeuroSymbolicSystem` prove the typestate rejects
use-before-init,
use-after-shutdown, and double-shutdown — `cargo test` fails if any
starts compiling.
- **0.1 panic-freedom + 0.2 numeric containment** on the core
operational paths:
  `neurophone-core/tests/proptest_core.rs`.
- `proofs/README.adoc` rewritten to reflect reality
(property/checked/open), and
corrected: the `spectral_radius` misnomer is **already fixed** in `esn`
(power
iteration), so 1.1's precondition holds — only the formal contraction
proof remains.
- `Justfile`: `proof-tla` (fetches `tla2tools.jar`, self-skips without
java), `proof`,
  and the RSR `quality` gate.

### Estate Trustfile (owner's explicit ask)
- `.machine_readable/contractiles/trust/Trustfile.a2ml` upgraded from 23
lines to the
full **A2ML Trustfile v2026.2.5-final** baseline, specialised for
neurophone: threat
model for an on-device app, real seams, the honest 0.1–3.2
`PROOF_ARTIFACTS` map with
explicit `non_claims`, capability gateway, crypto-agility. Owner-only
crypto
(Ed448+Dilithium5 / SPHINCS+, hashes, transparency entries) left as
`{{PLACEHOLDER}}`.
- New SHA-pinned `.github/workflows/trustfile.yml` gate: structural lint
+ placeholder
policy (WARN on branches / ERROR on main) + integrity-hash drift report
+ runnable checks.

Ground truth: `cargo test` **160 pass**, `cargo clippy --all-targets --
-D warnings`
clean, `cargo fmt --check` clean; TLC verified locally.

## FLAGS — external / owner-plane (unchanged)
- `gossamer` + `conative-gating` clones remain **403-blocked** → #83
epic and #103 staged.
- OPEN obligations 1.1 / 1.2 (formal) / 2.2 / 3.1 residual — honest,
with completion paths.
- Owner fills the Trustfile `{{PLACEHOLDER}}` crypto at signing time.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh

---
_Generated by [Claude
Code](https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh)_

---------

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.github/workflows/trustfile.yml

@@ -0,0 +1,81 @@
+# SPDX-License-Identifier: MPL-2.0
+# Validates the canonical Trustfile (estate baseline v2026.2.5-final) and runs
+# its fast integrity checks. Placeholder crypto tokens ({{...}}) are owner-supplied
+# at signing time, so they only hard-fail on `main` — on branches/PRs they warn.
+name: Trustfile Validation
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+jobs:
+  validate:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    env:
+      TRUSTFILE: .machine_readable/contractiles/trust/Trustfile.a2ml
+    steps:
+      - uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2
+        with:
+          persist-credentials: false
+
+      - name: Trustfile present and structurally complete
+        run: |
+          set -euo pipefail
+          test -f "$TRUSTFILE" || { echo "::error::$TRUSTFILE is missing"; exit 1; }
+          missing=""
+          for section in META THREAT_MODEL TRUSTFILE ESTATE_STANDARD \
+                         REPOSITORY_SPECIFIC PROOF_ARTIFACTS CAPABILITY_GATEWAY \
+                         CRYPTO_AGILITY SIGNATURE_BLOCK DEPLOYMENT; do
+            grep -qE "^### \[$section\]" "$TRUSTFILE" || missing="$missing $section"
+          done
+          if [ -n "$missing" ]; then
+            echo "::error::Trustfile missing required section(s):$missing"
+            exit 1
+          fi
+          echo "All required Trustfile sections present."
+
+      - name: Placeholder policy (WARN on branches, ERROR on main)
+        run: |
+          set -euo pipefail
+          count=$(grep -cE '\{\{[A-Za-z0-9_]+\}\}' "$TRUSTFILE" || true)
+          if [ "$count" -eq 0 ]; then
+            echo "No unresolved placeholders."
+            exit 0
+          fi
+          if [ "${GITHUB_REF:-}" = "refs/heads/main" ]; then
+            echo "::error::$count unresolved {{PLACEHOLDER}} token(s) on main — owner must fill crypto/provenance before release."
+            grep -nE '\{\{[A-Za-z0-9_]+\}\}' "$TRUSTFILE" | head -20
+            exit 1
+          else
+            echo "::warning::$count unresolved {{PLACEHOLDER}} token(s) (owner-supplied at signing time; allowed on branches)."
+          fi
+
+      - name: Integrity-hash drift report (informational)
+        run: |
+          set -euo pipefail
+          # Report the current digests so drift is visible; never auto-commit on a
+          # protected branch (that is a signing-time, owner-side step).
+          if command -v b3sum >/dev/null 2>&1; then echo "blake3:  $(b3sum "$TRUSTFILE" | awk '{print $1}')"; fi
+          echo "sha3-512: $(openssl dgst -sha3-512 "$TRUSTFILE" | awk '{print $2}')"
+
+      - name: Runnable integrity checks
+        run: |
+          set -euo pipefail
+          # license-content: sole-owner repo must be MPL-2.0
+          grep -q 'Mozilla Public License\|MPL-2.0' LICENSE \
+            || { echo "::error::LICENSE is not MPL-2.0"; exit 1; }
+          # no secrets committed
+          if [ -f .env ] || [ -f credentials.json ] || [ -f .env.local ]; then
+            echo "::error::secret/credential file committed"; exit 1
+          fi
+          echo "Runnable integrity checks passed."

.gitignore

@@ -84,3 +84,6 @@ deps/
 .cache/
 build/
 dist/
+
+# TLA+ model-checker jar cache (fetched by `just proof-tla`)
+.tlacache/