Merge branch 'main' into feat/gossamer-android-migration-83

Author: hyperpolymath

.gitignore

@@ -97,3 +97,10 @@ dist/
 
 # TLA+ model-checker jar cache (fetched by `just proof-tla`)
 .tlacache/
+
+# Dafny release cache (fetched by `just proof-dafny`)
+.dafnycache/
+
+# Lean/Lake build cache and vendored Mathlib checkout (fetched/built by
+# `just proof-lean`); see proofs/lean/.gitignore.
+proofs/lean/.lake/

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -225,22 +225,23 @@ artifacts:
   - id: "0.1" ; name: "Panic-freedom (operational paths)" ; system: "proptest" ; file: "crates/*/tests/proptest_*.rs, neurophone-core/tests/proptest_core.rs" ; status: "TESTED"
   - id: "0.2" ; name: "Numeric containment (no NaN/Inf)"   ; system: "proptest" ; file: "crates/*/tests/proptest_numeric.rs, proptest_core.rs"                  ; status: "TESTED"
   - id: "0.3" ; name: "unsafe discipline"                  ; system: "rustc"    ; file: "forbid/deny(unsafe_code) across crates"                                ; status: "PROVEN"
-  - id: "1.1" ; name: "Echo State Property"                ; system: "Lean/TLA" ; file: "proofs/lean/, proofs/tla/"                                             ; status: "DESIGNED"
-  - id: "1.2" ; name: "LSM bounded dynamics"               ; system: "proptest/Dafny" ; file: "crates/lsm/tests/proptest_bounds.rs"                             ; status: "TESTED"
+  - id: "1.1" ; name: "Echo State Property (contraction, ‖W‖∞ hypothesis)" ; system: "Lean 4 + Mathlib" ; file: "proofs/lean/EsnEcho.lean" ; status: "PROVEN"
+  - id: "1.2" ; name: "LSM bounded dynamics (membrane-potential ceiling)" ; system: "proptest + Dafny" ; file: "crates/lsm/tests/proptest_bounds.rs, proofs/dafny/LsmBoundedDynamics.dfy" ; status: "PROVEN"
   - id: "1.3" ; name: "Bridge soundness"                   ; system: "proptest" ; file: "crates/bridge/tests/proptest_soundness.rs"                             ; status: "TESTED"
   - id: "2.1" ; name: "Lifecycle state-machine safety"     ; system: "TLA+ (TLC)" ; file: "proofs/tla/Lifecycle.{tla,cfg}"                                      ; status: "PROVEN"
   - id: "2.2" ; name: "Concurrency safety"                 ; system: "TLA+"     ; file: "(deferred: single-owner design, no shared concurrency)"                ; status: "DESIGNED"
   - id: "2.3" ; name: "Resource/affine lifecycle"          ; system: "rustc (compile-fail)" ; file: "neurophone-core compile-fail doc-tests + android reset"       ; status: "PROVEN"
-  - id: "3.1" ; name: "Data-egress / privacy"              ; system: "arch + conative-gating" ; file: "claude-client (egress confined); veto external #103"        ; status: "DESIGNED"
+  - id: "3.1" ; name: "Data-egress / privacy"              ; system: "proptest + conative-gating" ; file: "crates/claude-client/src/egress_gate.rs (wired into create_message), egress_integration_tests" ; status: "TESTED"
   - id: "3.2" ; name: "Bounded external interaction"       ; system: "proptest/contract" ; file: "claude-client: capped backoff + bounded retries (backoff_is_bounded_and_monotonic, total_retry_budget_is_finite)" ; status: "TESTED"
 open_obligations:
-  - "1.1 formal contraction proof (precondition holds; theorem pending)"
-  - "1.2 formal Dafny bound (property evidence exists)"
+  - "1.1 bridge lemma: spectral_radius(W) < 1 (what esn::scale_to_spectral_radius actually enforces) does NOT in general imply ‖W‖∞ < 1 (the Lean theorem's hypothesis) for non-normal matrices — the contraction theorem itself is proven (proofs/lean/EsnEcho.lean), but this connecting lemma is a separate, harder, unattempted result (would need a Gelfand's-formula-style construction)."
+  - "1.2 the two-sided [reset, threshold] membrane-potential bound is FALSE in general (see the LowerBoundFails counterexample in proofs/dafny/LsmBoundedDynamics.dfy) — only the one-sided ceiling bound is provable and is now proven; the exact-real-vs-f32 gap and the spike-history-length bound (crates/lsm/tests/proptest_bounds.rs's third invariant) remain open, not attempted in Dafny this pass."
   - "2.2 concurrency spec (N/A until shared concurrency exists)"
-  - "3.1 GO/NO-GO egress veto (blocked on conative-gating, #103)"
+  - "3.1 caller-declared classification honesty (EgressClass is asserted by the caller, not derived from an independent sensor-provenance tracker); no formal (non-property) proof yet"
 non_claims:
-  - "neurophone does NOT yet claim a machine-checked Echo State Property (1.1)."
-  - "neurophone does NOT yet enforce a cryptographic egress veto (3.1)."
+  - "neurophone's 1.1 Lean proof (proofs/lean/EsnEcho.lean) establishes the classical reservoir contraction / echo-state theorem under a ‖W‖∞ < 1 hypothesis; it does NOT claim — and this is false in general for non-normal matrices — that the code's actual spectral-radius scaling implies that hypothesis. The code-to-theorem bridge is a separate, still-open lemma."
+  - "neurophone's 1.2 Dafny proof (proofs/dafny/LsmBoundedDynamics.dfy) establishes only a one-sided (ceiling) bound on membrane potential; it does NOT claim a lower (floor) bound (a Dafny counterexample refutes one), and it does not model f32 floating-point rounding, subnormals, or overflow."
+  - "neurophone's egress veto (3.1) enforces policy on a caller-declared payload classification; it does NOT independently verify that classification against real sensor provenance, and it is NOT a formally-proven (only property-tested) guarantee."
 
 ---
 ### [CI_CD]

Cargo.lock

@@ -81,10 +81,55 @@ proof-tla:
     cd proofs/tla
     java -XX:+UseParallelGC -cp "$jar" tlc2.TLC -config Lifecycle.cfg Lifecycle.tla
 
+# Type-check the Lean 4 Echo State Property proof (obligation 1.1, issue
+# #84, `proofs/lean/EsnEcho.lean`). Self-skips (non-fatal) if `lake` (elan)
+# isn't on PATH. First run needs network access to fetch the pinned Mathlib
+# revision (see `proofs/lean/lake-manifest.json`); later runs reuse the
+# local `.lake/` cache.
+proof-lean:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if ! command -v lake >/dev/null 2>&1; then
+        echo "proof-lean: lake not found — skipping Lean check (spec unchanged)"; exit 0
+    fi
+    cd proofs/lean && lake build
+
+# Verify the Dafny LSM-bounded-dynamics proof (obligation 1.2, issue #84,
+# `proofs/dafny/LsmBoundedDynamics.dfy`). Uses a system `dafny` if present;
+# otherwise fetches a pinned, checksum-verified, self-contained release into
+# `.dafnycache/` on first run. Self-skips (non-fatal) if no system `dafny`
+# is found and the download isn't possible (offline / no permissions), so
+# it degrades gracefully in minimal/offline environments.
+proof-dafny:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if command -v dafny >/dev/null 2>&1; then
+        dafny verify proofs/dafny/LsmBoundedDynamics.dfy
+        exit 0
+    fi
+    version=4.11.0
+    sha256=a46a9ff7cdd720f7955854c78e95df13f4cfe6b80691b05f8654fe19e8267179
+    dir="$(pwd)/.dafnycache/dafny-${version}"
+    bin="${dir}/dafny/dafny"
+    if [ ! -x "$bin" ]; then
+        zip="$(pwd)/.dafnycache/dafny-${version}.zip"
+        mkdir -p "$dir"
+        if ! curl -fsSL -o "$zip" \
+          "https://github.com/dafny-lang/dafny/releases/download/v${version}/dafny-${version}-x64-ubuntu-22.04.zip"; then
+            echo "proof-dafny: could not download Dafny (offline?) — skipping"; exit 0
+        fi
+        echo "${sha256}  ${zip}" | sha256sum -c - || {
+            echo "proof-dafny: checksum mismatch on downloaded release, aborting"; exit 1
+        }
+        unzip -q "$zip" -d "$dir"
+    fi
+    "$bin" verify proofs/dafny/LsmBoundedDynamics.dfy
+
 # Run the full proof surface: property tests + compile-fail typestate doc-tests
-# (via `cargo test`) plus the TLA+ model check.
-proof: test proof-tla
-    @echo "Proof surface checked (properties, typestate compile-fails, TLC)."
+# (via `cargo test`) plus the TLA+ model check, the Lean type-check, and the
+# Dafny verification.
+proof: test proof-tla proof-lean proof-dafny
+    @echo "Proof surface checked (properties, typestate compile-fails, TLC, Lean, Dafny)."
 
 # Quality gates (RSR golden path `just test && just quality`).
 quality: fmt-check lint audit

Justfile

@@ -0,0 +1,48 @@
+; SPDX-License-Identifier: MPL-2.0
+; assail-classifications.a2ml — user-classification registry for panic-attack.
+;
+; Flips audited-sound findings to `suppressed = true` AFTER the kanren
+; structural-suppression pass (see panic-attack src/assail/mod.rs ::
+; apply_user_classifications). Matching is exact on (file, category). This
+; registry lives apart from the source under scan, so a finding cannot
+; self-suppress — each entry is a reviewable companion change with a rationale
+; cross-referenced to audits/audit-install-scripts.adoc.
+;
+; All entries below are audited false positives; neurophone has 0 real
+; vulnerabilities (production: 0 unsafe, 0 panic sites, 0 injection, 0 crypto
+; misuse). The PanicPath findings are auto-suppressed (test/bench) and need no
+; classification here.
+;
+; The top-level identity/version fields below satisfy the estate a2ml-validate
+; gate (matching a2ml-ecosystem conformance/valid/sectioned-manifest.a2ml);
+; panic-attack's loader ignores everything outside `(classification …)` blocks,
+; so they do not affect suppression.
+
+project = "neurophone"
+schema_version = "1.0.0"
+
+[metadata]
+name = "assail-classifications"
+version = "1.0.0"
+
+(assail-classifications
+  (classification
+    (file "scripts/setup.sh")
+    (category "PathTraversal")
+    (audit "audits/audit-install-scripts.adoc §1")
+    (rationale "Android /data/local/tmp device-staging path (adb), not host /tmp"))
+  (classification
+    (file "scripts/install-on-phone.sh")
+    (category "PathTraversal")
+    (audit "audits/audit-install-scripts.adoc §1")
+    (rationale "adb push target on the device: /data/local/tmp/<model>, not host /tmp"))
+  (classification
+    (file "scripts/uninstall.sh")
+    (category "PathTraversal")
+    (audit "audits/audit-install-scripts.adoc §1")
+    (rationale "adb shell rm of the on-device model at /data/local/tmp, not host /tmp"))
+  (classification
+    (file "scripts/install-termux.sh")
+    (category "HardcodedSecret")
+    (audit "audits/audit-install-scripts.adoc §2")
+    (rationale "public HuggingFace model URL + commented sk-ant placeholder in a config template; no secret")))

audits/assail-classifications.a2ml

@@ -0,0 +1,45 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= Audit: install/uninstall shell scripts — panic-attack residuals
+:toc:
+:revdate: 2026-07-01
+
+Companion audit for `audits/assail-classifications.a2ml`. Records why the
+`panic-attack assail` findings in the install/uninstall shell scripts are
+audited-sound false positives, so they may be classified `suppressed` in a
+reviewable, out-of-band way (per the panic-attack user-classification pattern —
+the registry lives apart from the source, so a finding cannot self-suppress).
+
+Scan of record: `panic-attack assail .` — 9 weak points, 0 real vulnerabilities.
+The 5 `PanicPath` findings are already auto-suppressed (test/bench code). The
+four production-script findings below are the audited residuals.
+
+== §1 PathTraversal — Android device-staging paths (not host `/tmp`)
+
+Files: `scripts/setup.sh`, `scripts/install-on-phone.sh`, `scripts/uninstall.sh`.
+
+The detector pattern-matched `/tmp/` inside `/data/local/tmp/`. That is **not**
+the host temp directory — it is the canonical Android **on-device** staging path
+used with `adb push` / `adb shell`, the standard location for pushing a model
+file to a phone:
+
+* `scripts/setup.sh` — an `echo` instruction: `Place in: /data/local/tmp/ on the device`.
+* `scripts/install-on-phone.sh` — `DEVICE_MODEL_PATH="/data/local/tmp/${MODEL_FILE}"`, the `adb push` target on the device.
+* `scripts/uninstall.sh` — `adb shell rm -f /data/local/tmp/llama-…gguf`, removing the model from the device.
+
+There is no host-side symlink/traversal surface here: the path is a device path
+addressed through `adb`, and applying `mktemp` would be **incorrect** (you cannot
+`mktemp` a device path, and `/data/local/tmp/` is the required Android location).
+Classification: audited-sound false positive.
+
+== §2 HardcodedSecret — public URL + commented key template
+
+File: `scripts/install-termux.sh`.
+
+* Line ~19: `MODEL_URL="https://huggingface.co/…/Llama-3.2-1B-Instruct-Q4_K_M.gguf"` — a **public** model download URL, not a secret.
+* The `sk-ant-…` string is a **commented-out placeholder** inside a generated
+  `config.toml` template (`# api_key = "sk-ant-..."   # uncomment + set …`),
+  showing the user where to place *their own* key. No credential is committed.
+
+No secret enters source control (corroborated by the estate secret-scanner gate).
+Classification: audited-sound false positive.

audits/audit-install-scripts.adoc

@@ -13,6 +13,13 @@ tracing = { workspace = true }
 tokio = { workspace = true }
 reqwest = { workspace = true }
 futures = { workspace = true }
+uuid = { version = "1", features = ["v4"] }
+# conative-gating is pre-1.0 (0.1.0) and not published to crates.io, so it is
+# consumed as a git dependency pinned to a specific commit SHA on the public
+# hyperpolymath/conative-gating repo (issue #103 / proof obligation 3.1:
+# egress GO/NO-GO veto). Do NOT float on a branch -- re-pin deliberately.
+policy-oracle = { git = "https://github.com/hyperpolymath/conative-gating", rev = "7baaf25ecb20ec2a75f138ec69c1681e7677021a" }
+gating-contract = { git = "https://github.com/hyperpolymath/conative-gating", rev = "7baaf25ecb20ec2a75f138ec69c1681e7677021a" }
 
 [dev-dependencies]
 tokio = { workspace = true, features = ["rt-multi-thread", "macros"] }