proof(#84): discharge 3.2 bounded external interaction (property)

.machine_readable/6a2/STATE.a2ml

@@ -41,8 +41,8 @@ neurophone-android = "implemented — 11-method ai.neurophone.NativeLib JNI surf
 
 [proofs]
 # Honest obligation status; full detail in proofs/README.adoc + Trustfile PROOF_ARTIFACTS.
-discharged = "0.1 panic-freedom, 0.2 numeric containment, 0.3 unsafe discipline, 1.2 LSM bounds, 1.3 bridge soundness (property); 2.1 lifecycle (TLC); 2.3 release-once (compile-fail)"
-open = "1.1 Echo State Property (formal contraction), 1.2 formal Dafny bound, 2.2 concurrency (N/A single-owner), 3.1 egress veto (external #103), 3.2 bounded-interaction contract test"
+discharged = "0.1 panic-freedom, 0.2 numeric containment, 0.3 unsafe discipline, 1.2 LSM bounds, 1.3 bridge soundness, 3.2 bounded external interaction (property); 2.1 lifecycle (TLC); 2.3 release-once (compile-fail)"
+open = "1.1 Echo State Property (formal contraction), 1.2 formal Dafny bound, 2.2 concurrency (N/A single-owner), 3.1 egress veto (external #103)"
 
 [recent-work]
 session-date = "2026-07-01"

.machine_readable/contractiles/trust/Trustfile.a2ml

@@ -232,7 +232,7 @@ artifacts:
   - 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.2" ; name: "Bounded external interaction"       ; system: "contract test" ; file: "SystemConfig.max_response_time_ms (test pending)"                ; status: "DESIGNED"
+  - 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)"

crates/claude-client/src/lib.rs

@@ -660,6 +660,27 @@ mod tests {
         }
     }
 
+    #[test]
+    fn total_retry_budget_is_finite() {
+        // 3.2 (bounded external interaction): the retry loop runs a *bounded*
+        // number of attempts (`for attempt in 0..=max_retries`), and each wait is
+        // the capped backoff — so the worst-case total wait across the whole
+        // interaction is finite and bounded, not just each individual delay.
+        let max_retries = ClaudeConfig::default().max_retries;
+        let mut total = Duration::ZERO;
+        for a in 0..=(max_retries as u32) {
+            total = total
+                .checked_add(ClaudeClient::backoff_delay(a))
+                .expect("total backoff must not overflow");
+        }
+        // (max_retries + 1) attempts, each capped at 60s.
+        let ceiling = Duration::from_secs(60) * (max_retries as u32 + 1);
+        assert!(
+            total <= ceiling,
+            "total retry budget {total:?} exceeds bound {ceiling:?}"
+        );
+    }
+
     #[test]
     fn user_content_cannot_inject_into_request_json() {
         // 3.2: user content is typed JSON, so quotes/braces are escaped and cannot

proofs/README.adoc

@@ -20,7 +20,7 @@ the index from each obligation to the artefact that discharges it.
 | TLA+ (TLC)        | `proofs/tla/`   | 2.1 lifecycle *(checked)*; 2.2/3.1 specs deferred
 | Lean / Coq        | `proofs/lean/`  | 1.1 echo state property, 1.3 bridge soundness (spec)
 | Dafny / F*        | `proofs/dafny/` | 1.2 LSM bounded dynamics, 0.2 numeric containment (spec)
-| proptest          | (in `crates/`)  | executable evidence for 0.1, 0.2, 1.2, 1.3
+| proptest          | (in `crates/`)  | executable evidence for 0.1, 0.2, 1.2, 1.3, 3.2
 | compile-fail tests| `neurophone-core` doc-tests | 2.1 (type level) + 2.3 release-once
 |===
 
@@ -46,7 +46,7 @@ by property tests over the operational paths; *open* = honest gap, never faked.
 | 2.2 | Concurrency safety (no deadlock)                | *open* — N/A under the current single-owner (`&mut`) design; TLA+ spec deferred until shared concurrency exists
 | 2.3 | Resource/affine lifecycle                       | *checked* (release-once) — `shutdown(self)` consumes the system; compile-fail doc-tests reject double-shutdown / use-after-shutdown; wired through the JNI holder's `reset`. Linear *must-use* (guaranteed shutdown) *open* (needs AffineScript)
 | 3.1 | Data-egress / privacy invariant                 | *open* — egress is confined to `claude-client` by construction; the GO/NO-GO veto is external `conative-gating` (#103)
-| 3.2 | Bounded external interaction                    | *open* — `SystemConfig.max_response_time_ms` bounds exist; a dedicated contract test is pending
+| 3.2 | Bounded external interaction                    | *property* — `claude-client`: capped saturating `backoff_delay` + bounded `max_retries` retry loop; tests `backoff_is_bounded_and_monotonic`, `total_retry_budget_is_finite` (whole interaction has a finite time bound), `user_content_cannot_inject_into_request_json`
 |===
 
 [NOTE]