diff --git a/.machine_readable/contractiles/trust/Trustfile.a2ml b/.machine_readable/contractiles/trust/Trustfile.a2ml index d31680f..f3f1cc4 100644 --- a/.machine_readable/contractiles/trust/Trustfile.a2ml +++ b/.machine_readable/contractiles/trust/Trustfile.a2ml @@ -231,16 +231,16 @@ artifacts: - 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)" - "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 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] diff --git a/Cargo.lock b/Cargo.lock index 0d4f8ac..4bb5015 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -271,7 +271,9 @@ version = "1.0.0" dependencies = [ "criterion", "futures", + "gating-contract", "ndarray", + "policy-oracle", "proptest", "reqwest", "serde", @@ -279,6 +281,7 @@ dependencies = [ "thiserror 2.0.18", "tokio", "tracing", + "uuid", ] [[package]] @@ -575,6 +578,21 @@ dependencies = [ "slab", ] +[[package]] +name = "gating-contract" +version = "0.1.0" +source = "git+https://github.com/hyperpolymath/conative-gating?rev=7baaf25ecb20ec2a75f138ec69c1681e7677021a#7baaf25ecb20ec2a75f138ec69c1681e7677021a" +dependencies = [ + "chrono", + "policy-oracle", + "serde", + "serde_json", + "slm-evaluator", + "thiserror 2.0.18", + "tracing", + "uuid", +] + [[package]] name = "getrandom" version = "0.2.17" @@ -615,6 +633,12 @@ dependencies = [ "wasip3", ] +[[package]] +name = "glob" +version = "0.3.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0cc23270f6e1808e30a928bdc84dea0b9b4136a8bc82338574f23baf47bbd280" + [[package]] name = "half" version = "2.7.1" @@ -1339,6 +1363,21 @@ dependencies = [ "plotters-backend", ] +[[package]] +name = "policy-oracle" +version = "0.1.0" +source = "git+https://github.com/hyperpolymath/conative-gating?rev=7baaf25ecb20ec2a75f138ec69c1681e7677021a#7baaf25ecb20ec2a75f138ec69c1681e7677021a" +dependencies = [ + "glob", + "regex", + "serde", + "serde_json", + "thiserror 2.0.18", + "tokio", + "tracing", + "uuid", +] + [[package]] name = "portable-atomic" version = "1.13.1" @@ -1935,6 +1974,19 @@ version = "0.4.12" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" +[[package]] +name = "slm-evaluator" +version = "0.1.0" +source = "git+https://github.com/hyperpolymath/conative-gating?rev=7baaf25ecb20ec2a75f138ec69c1681e7677021a#7baaf25ecb20ec2a75f138ec69c1681e7677021a" +dependencies = [ + "serde", + "serde_json", + "thiserror 2.0.18", + "tokio", + "tracing", + "uuid", +] + [[package]] name = "smallvec" version = "1.15.1" @@ -2283,6 +2335,18 @@ version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "b6c140620e7ffbb22c2dee59cafe6084a59b5ffc27a8859a5f0d494b5d52b6be" +[[package]] +name = "uuid" +version = "1.23.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bf80a72845275afea99e7f2b434723d3bc7e38470fcd1c7ed39a599c73319a53" +dependencies = [ + "getrandom 0.4.2", + "js-sys", + "serde_core", + "wasm-bindgen", +] + [[package]] name = "valuable" version = "0.1.1" diff --git a/crates/claude-client/Cargo.toml b/crates/claude-client/Cargo.toml index 8627be7..fc7a66c 100644 --- a/crates/claude-client/Cargo.toml +++ b/crates/claude-client/Cargo.toml @@ -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"] } diff --git a/crates/claude-client/src/egress_gate.rs b/crates/claude-client/src/egress_gate.rs new file mode 100644 index 0000000..5d45682 --- /dev/null +++ b/crates/claude-client/src/egress_gate.rs @@ -0,0 +1,308 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell +//! Cloud-egress GO/NO-GO veto (issue #103, proof obligation 3.1). +//! +//! Wraps `hyperpolymath/conative-gating`'s `gating-contract` crate as the +//! policy layer that must approve any payload before it is allowed to leave +//! the device over the network. The veto is synchronous, deterministic and +//! fast (the underlying oracle is a plain rule/regex scan, no ML), so it can +//! sit directly in front of every outbound network call without meaningfully +//! affecting latency. +//! +//! ## Adapting `gating-contract` to network egress +//! +//! `gating-contract`'s `GatingRequest`/`Proposal` types are shaped for +//! *code-proposal* gating (a candidate file edit/command, not a network +//! payload) and there is no `ActionType::NetworkEgress` variant upstream. +//! Rather than force a fictitious fit or fork conative-gating (explicitly +//! out of scope per issue #103), this module makes a deliberate, documented +//! mapping: +//! +//! - `ActionType::ExecuteCommand { command }` represents "attempt to send +//! this payload to `destination`" (`command = "network-egress:"`). +//! This is the closest existing variant to "perform an external-effect +//! action"; it is not a perfect fit, but it is honest about what it means +//! (no new upstream variant was invented for this). +//! - `Proposal.content` carries the *literal outbound payload text* (system +//! prompt + message bodies), so the oracle's generic content-scanning +//! rules (e.g. hardcoded-secret patterns) really do run against what would +//! go over the wire. +//! - `Proposal.files_affected` carries a synthetic `egress://` +//! locator, purely so the audit trail records *where* the payload was +//! headed (there is no real file). +//! - The caller-supplied [`EgressClass`] (raw sensor / raw neural state / +//! derived inference / plain user text) is encoded as a literal +//! `[[EGRESS_CLASS:...]]` marker prepended to `content`. This is a real use +//! of the oracle's actual mechanism (a configured regex over `content`), +//! not a bypass of it: `egress_policy()` below is a bespoke +//! `Policy` (NOT `Policy::rsr_default()`, which is a source-code-hygiene +//! policy about forbidden languages/toolchains and has nothing useful to +//! say about a network payload) whose only forbidden patterns are (a) the +//! raw-sensor/raw-neural-state marker and (b) the same hardcoded-secret +//! regex `rsr_default()` uses, reused here as defense-in-depth against a +//! credential accidentally ending up in outbound message text. +//! +//! ## Honesty about the classification boundary +//! +//! [`EgressClass`] is **caller-declared**: this module cannot itself prove +//! that a payload labelled `DerivedInference` really is an aggregate rather +//! than raw sensor data relabelled by mistake -- that would require real +//! sensor-provenance tracking, which does not exist yet in this repo. What +//! this gate *does* guarantee is: whatever class is declared, `RawSensor` +//! and `RawNeuralState` are always blocked, and the hardcoded-secret check +//! always runs regardless of the declared class. +use gating_contract::{ContractError, ContractRunner, GatingDecision, GatingRequest, Verdict}; +use policy_oracle::{ + ActionType, EnforcementConfig, ForbiddenPattern, LanguagePolicy, PatternPolicy, Policy, + Proposal, ToolchainPolicy, +}; +use uuid::Uuid; + +/// Coarse, caller-declared sensitivity classification for an outbound +/// payload. See the module-level docs for the honesty caveat: this is a +/// declaration, not a proof. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum EgressClass { + /// Unprocessed sensor readings (accelerometer/mic/etc.) -- must never + /// leave the device. + RawSensor, + /// Reservoir/neural internal state that directly reflects raw sensor + /// input 1:1 (not yet aggregated/summarised) -- must never leave the + /// device. + RawNeuralState, + /// A derived or aggregated inference over neural/sensor state (e.g. a + /// summarised description) -- may leave the device. + DerivedInference, + /// Plain user-authored text with no sensor provenance -- may leave the + /// device. + UserText, +} + +impl EgressClass { + fn marker(self) -> &'static str { + match self { + EgressClass::RawSensor => "RAW_SENSOR", + EgressClass::RawNeuralState => "RAW_NEURAL_STATE", + EgressClass::DerivedInference => "DERIVED_INFERENCE", + EgressClass::UserText => "USER_TEXT", + } + } +} + +/// Errors from the egress veto stage. Distinguished from [`crate::ClaudeError`] +/// so callers can tell "the network call itself failed" apart from "the +/// network call was never attempted because policy said no". +#[derive(Debug, thiserror::Error)] +pub enum EgressGateError { + /// Hard NO-GO: the payload must not be sent. Not overridable from here. + #[error("egress blocked by policy: {reason}")] + Blocked { reason: String }, + /// The policy engine wants a human decision before this can proceed. + /// `ContractRunner::evaluate` does not currently produce this verdict + /// (no arbiter/escalation stage is wired up yet upstream), but it is + /// handled here so this gate fails closed rather than silently allowing + /// a future `Escalate` verdict through. + #[error("egress escalated for human review: {reason}")] + Escalated { reason: String }, + /// The gating contract itself errored (e.g. an invalid regex in the + /// policy) -- fails closed, never falls through to "allowed". + #[error("gating contract error: {0}")] + Contract(#[from] ContractError), +} + +/// Policy tailored for network-egress veto decisions (obligation 3.1). +/// Deliberately not `Policy::rsr_default()` -- see the module docs. +fn egress_policy() -> Policy { + Policy { + name: "neurophone-egress-veto".to_string(), + languages: LanguagePolicy::default(), + toolchain: ToolchainPolicy::default(), + patterns: PatternPolicy { + forbidden_patterns: vec![ + ForbiddenPattern { + name: "raw_sensor_egress".to_string(), + regex: r"\[\[EGRESS_CLASS:(RAW_SENSOR|RAW_NEURAL_STATE)\]\]".to_string(), + file_types: vec!["*".to_string()], + reason: "Raw/unaggregated sensor-derived data must never leave the device (obligation 3.1)" + .to_string(), + }, + ForbiddenPattern { + // Same rule `Policy::rsr_default()` uses for source code; + // reused here as defense-in-depth against a credential + // accidentally ending up in outbound message text. + name: "hardcoded_secrets".to_string(), + regex: r#"(?i)(password|secret|api_key)\s*=\s*["'][^"']{8,}["']"#.to_string(), + file_types: vec!["*".to_string()], + reason: "Hardcoded secret detected in outbound payload".to_string(), + }, + ], + }, + enforcement: EnforcementConfig::default(), + } +} + +/// GO/NO-GO veto for outbound network calls, backed by `conative-gating`'s +/// `gating-contract` crate. +pub struct EgressGate { + runner: ContractRunner, +} + +impl EgressGate { + /// Build the gate with the bespoke `egress_policy()`. + pub fn new() -> Self { + Self { + runner: ContractRunner::with_policy(egress_policy()), + } + } + + /// Evaluate whether `content`, classified as `class`, may be sent to + /// `destination`. Returns `Ok(GatingDecision)` when the verdict is + /// `Allow`/`Warn` (i.e. `Verdict::is_allowed()`); `Err` otherwise. Callers + /// MUST NOT perform the network call unless this returns `Ok`. + pub fn check( + &self, + class: EgressClass, + destination: &str, + content: &str, + ) -> Result { + let tagged = format!("[[EGRESS_CLASS:{}]]\n{}", class.marker(), content); + let proposal = Proposal { + id: Uuid::new_v4(), + action_type: ActionType::ExecuteCommand { + command: format!("network-egress:{destination}"), + }, + content: tagged, + files_affected: vec![format!("egress://{destination}")], + // Unused by `ContractRunner::evaluate` today (only the oracle + // stage runs; the SLM stage that would consume this confidence + // score is an unimplemented stub upstream). Set to 1.0 as an + // honest "not applicable" placeholder rather than a fabricated + // confidence value. + llm_confidence: 1.0, + }; + let request = GatingRequest::new(proposal); + let decision = self.runner.evaluate(&request)?; + let audit = self.runner.audit(&request, &decision); + + match decision.verdict { + Verdict::Allow => { + tracing::debug!(request_id = %audit.request_id, "egress allowed"); + Ok(decision) + } + Verdict::Warn => { + let reason = decision + .refusal + .as_ref() + .map(|r| r.message.clone()) + .unwrap_or_default(); + tracing::warn!(request_id = %audit.request_id, %reason, "egress allowed with policy warning"); + Ok(decision) + } + Verdict::Block => { + let reason = decision + .refusal + .as_ref() + .map(|r| r.message.clone()) + .unwrap_or_else(|| "blocked by policy".to_string()); + tracing::warn!(request_id = %audit.request_id, %reason, "egress BLOCKED by policy veto"); + Err(EgressGateError::Blocked { reason }) + } + Verdict::Escalate => { + let reason = decision + .refusal + .as_ref() + .map(|r| r.message.clone()) + .unwrap_or_else(|| "escalation required".to_string()); + tracing::warn!(request_id = %audit.request_id, %reason, "egress ESCALATED for human review"); + Err(EgressGateError::Escalated { reason }) + } + } + } +} + +impl Default for EgressGate { + fn default() -> Self { + Self::new() + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn raw_sensor_is_blocked() { + let gate = EgressGate::new(); + let err = gate + .check( + EgressClass::RawSensor, + "api.anthropic.com", + "accel=[0.1,0.2,9.8]", + ) + .expect_err("raw sensor data must be blocked"); + assert!(matches!(err, EgressGateError::Blocked { .. })); + } + + #[test] + fn raw_neural_state_is_blocked() { + let gate = EgressGate::new(); + let err = gate + .check( + EgressClass::RawNeuralState, + "api.anthropic.com", + "reservoir_state=[0.02, -0.87, 0.4, ...]", + ) + .expect_err("raw neural state must be blocked"); + assert!(matches!(err, EgressGateError::Blocked { .. })); + } + + #[test] + fn derived_inference_is_allowed() { + let gate = EgressGate::new(); + let decision = gate + .check( + EgressClass::DerivedInference, + "api.anthropic.com", + "the user appears calm and focused", + ) + .expect("derived/aggregated inference should be allowed"); + assert_eq!(decision.verdict, Verdict::Allow); + } + + #[test] + fn user_text_is_allowed() { + let gate = EgressGate::new(); + let decision = gate + .check( + EgressClass::UserText, + "api.anthropic.com", + "what time is it?", + ) + .expect("plain user text should be allowed"); + assert_eq!(decision.verdict, Verdict::Allow); + } + + #[test] + fn hardcoded_secret_is_blocked_even_in_an_otherwise_allowed_class() { + let gate = EgressGate::new(); + let err = gate + .check( + EgressClass::UserText, + "api.anthropic.com", + r#"api_key = "sk-not-a-real-secret-value""#, + ) + .expect_err("hardcoded-secret pattern must block regardless of declared class"); + assert!(matches!(err, EgressGateError::Blocked { .. })); + } + + #[test] + fn decision_carries_a_stable_request_id_for_audit_correlation() { + let gate = EgressGate::new(); + let decision = gate + .check(EgressClass::UserText, "api.anthropic.com", "hi") + .unwrap(); + // request_id round-trips through GatingRequest -> GatingDecision, which + // is what lets an AuditEntry correlate back to the original request. + assert_ne!(decision.request_id, Uuid::nil()); + } +} diff --git a/crates/claude-client/src/lib.rs b/crates/claude-client/src/lib.rs index 03c55b2..75a76f1 100644 --- a/crates/claude-client/src/lib.rs +++ b/crates/claude-client/src/lib.rs @@ -1,4 +1,5 @@ // SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell //! Claude API Client - Cloud Connection //! //! Connects to Claude (Anthropic's AI) for advanced reasoning @@ -19,6 +20,9 @@ use std::time::Duration; use thiserror::Error; use tracing::{debug, warn}; +pub mod egress_gate; +pub use egress_gate::{EgressClass, EgressGate, EgressGateError}; + /// Claude API errors #[derive(Error, Debug)] pub enum ClaudeError { @@ -36,6 +40,11 @@ pub enum ClaudeError { Timeout, #[error("Configuration error: {0}")] ConfigError(String), + /// Obligation 3.1: the egress GO/NO-GO veto refused this payload. The + /// network call is guaranteed to NOT have been attempted when this + /// variant is returned -- see `ClaudeClient::create_message`. + #[error("egress denied by policy veto: {0}")] + EgressDenied(#[from] EgressGateError), } /// Claude model variants @@ -210,6 +219,10 @@ pub struct ClaudeClient { config: ClaudeConfig, client: Client, conversation_history: Vec, + /// Obligation 3.1: every outbound call goes through this veto first -- + /// see `create_message`, the single choke point that actually performs + /// the network request. + egress: EgressGate, } impl ClaudeClient { @@ -228,6 +241,7 @@ impl ClaudeClient { config, client, conversation_history: Vec::new(), + egress: EgressGate::new(), }) } @@ -236,10 +250,14 @@ impl ClaudeClient { Self::new(ClaudeConfig::default()) } - /// Send a simple message and get response + /// Send a simple message and get response. Classified as plain user text + /// for the egress veto (obligation 3.1) -- it carries no sensor/neural + /// provenance. pub async fn send_message(&mut self, content: &str) -> Result { let messages = vec![Message::user(content)]; - let response = self.create_message(messages, None).await?; + let response = self + .create_message(messages, None, EgressClass::UserText) + .await?; // Extract text from response let text = response @@ -256,17 +274,24 @@ impl ClaudeClient { Ok(text) } - /// Send message with neural context + /// Send message with neural context. `class` is the caller's declared + /// classification of `neural_context` for the egress veto (obligation + /// 3.1) -- e.g. `EgressClass::RawNeuralState` if it is raw reservoir + /// state, `EgressClass::DerivedInference` if it has already been + /// summarised/aggregated. The veto enforces policy on whatever is + /// declared; it cannot independently prove the declaration is honest + /// (see `egress_gate` module docs). pub async fn send_message_with_context( &mut self, content: &str, neural_context: &str, + class: EgressClass, ) -> Result { // Prepend neural context to the system prompt (only when enabled). let system = self.build_system(neural_context); let messages = vec![Message::user(content)]; - let response = self.create_message(messages, system).await?; + let response = self.create_message(messages, system, class).await?; let text = response .content @@ -278,7 +303,9 @@ impl ClaudeClient { Ok(text) } - /// Continue conversation with history + /// Continue conversation with history. Classified as plain user text for + /// the egress veto (obligation 3.1); this method has no neural-context + /// parameter to begin with. pub async fn chat(&mut self, content: &str) -> Result { self.conversation_history.push(Message::user(content)); @@ -286,6 +313,7 @@ impl ClaudeClient { .create_message( self.conversation_history.clone(), self.config.system_prompt.clone(), + EgressClass::UserText, ) .await?; @@ -301,14 +329,26 @@ impl ClaudeClient { Ok(text) } - /// Create a message with full control + /// Create a message with full control. + /// + /// This is the single choke point that performs the actual outbound + /// HTTP request to the Claude API (every other method funnels through + /// here). Obligation 3.1: the egress veto runs first, against the exact + /// text that is about to be serialized onto the wire; on `Block`/ + /// `Escalate` this returns `Err(ClaudeError::EgressDenied(_))` and the + /// network call is never made. pub async fn create_message( &self, messages: Vec, system: Option, + class: EgressClass, ) -> Result { let api_key = self.config.api_key.as_ref().ok_or(ClaudeError::NoApiKey)?; + let outbound_text = Self::render_outbound_text(&system, &messages); + self.egress + .check(class, &self.config.base_url, &outbound_text)?; + let request = CreateMessageRequest { model: self.config.model.as_str().to_string(), max_tokens: 1024, @@ -407,6 +447,26 @@ impl ClaudeClient { } } + /// Render exactly the text that `create_message` is about to serialize + /// onto the wire (system prompt + all message bodies), for the egress + /// veto (obligation 3.1) to scan. Kept separate from JSON construction so + /// the veto sees plain text, not the JSON envelope. + fn render_outbound_text(system: &Option, messages: &[Message]) -> String { + let mut text = String::new(); + if let Some(sys) = system { + text.push_str(sys); + text.push('\n'); + } + for message in messages { + for block in &message.content { + let ContentBlock::Text { text: block_text } = block; + text.push_str(block_text); + text.push('\n'); + } + } + text + } + /// Exponential backoff for retry `attempt`, saturating and capped at 60s so /// it can never overflow or wait unboundedly (obligation 3.2). fn backoff_delay(attempt: u32) -> Duration { @@ -706,3 +766,111 @@ mod tests { ); } } + +/// Obligation 3.1: end-to-end proof that the egress veto actually gates the +/// real network call inside `create_message`, not just the standalone +/// `EgressGate` unit (see `egress_gate::tests`). +/// +/// Rather than adding a mocking framework/transport-trait abstraction, these +/// tests spin up a tiny real HTTP/1.1 server on loopback that counts +/// accepted connections. `ClaudeClient` is pointed at it via `base_url` and +/// makes real `reqwest` calls against it -- so "zero calls" here means +/// literally zero TCP connections were made to the (fake) API, not "a mock +/// was not invoked". +#[cfg(test)] +mod egress_integration_tests { + use super::*; + use std::sync::atomic::{AtomicUsize, Ordering}; + use std::sync::Arc; + + /// A minimal, valid `MessageResponse` JSON body. + const FAKE_RESPONSE_BODY: &str = r#"{"id":"msg_test","type":"message","role":"assistant","content":[{"type":"text","text":"ok"}],"model":"m","stop_reason":null,"stop_sequence":null,"usage":{"input_tokens":1,"output_tokens":1}}"#; + + /// Spawn a fake Claude API endpoint on `127.0.0.1` that counts every + /// accepted connection and replies with `FAKE_RESPONSE_BODY`. Returns the + /// `http://host:port` base URL and a shared call counter. + async fn spawn_fake_claude_server() -> (String, Arc) { + use tokio::io::{AsyncReadExt, AsyncWriteExt}; + + let listener = tokio::net::TcpListener::bind("127.0.0.1:0") + .await + .expect("bind loopback listener"); + let addr = listener.local_addr().expect("read local addr"); + let calls = Arc::new(AtomicUsize::new(0)); + let calls_for_task = calls.clone(); + + tokio::spawn(async move { + loop { + let Ok((mut socket, _)) = listener.accept().await else { + break; + }; + calls_for_task.fetch_add(1, Ordering::SeqCst); + tokio::spawn(async move { + let mut buf = vec![0u8; 8192]; + // Best-effort read of the request; we don't need to parse + // it, just drain enough that reqwest sees a response. + let _ = socket.read(&mut buf).await; + let response = format!( + "HTTP/1.1 200 OK\r\nContent-Type: application/json\r\nContent-Length: {}\r\nConnection: close\r\n\r\n{}", + FAKE_RESPONSE_BODY.len(), + FAKE_RESPONSE_BODY + ); + let _ = socket.write_all(response.as_bytes()).await; + let _ = socket.shutdown().await; + }); + } + }); + + (format!("http://{addr}"), calls) + } + + fn test_config(base_url: String) -> ClaudeConfig { + ClaudeConfig { + api_key: Some("test-key".to_string()), + base_url, + max_retries: 0, + ..Default::default() + } + } + + #[tokio::test] + async fn blocked_egress_never_reaches_the_network() { + let (base_url, calls) = spawn_fake_claude_server().await; + let client = ClaudeClient::new(test_config(base_url)).expect("client config is valid"); + + let result = client + .create_message( + vec![Message::user("raw sensor payload")], + None, + EgressClass::RawSensor, + ) + .await; + + assert!( + matches!(result, Err(ClaudeError::EgressDenied(_))), + "expected EgressDenied, got {result:?}" + ); + assert_eq!( + calls.load(Ordering::SeqCst), + 0, + "a blocked request must never open a connection to the transport" + ); + } + + #[tokio::test] + async fn allowed_egress_reaches_the_network_exactly_once() { + let (base_url, calls) = spawn_fake_claude_server().await; + let client = ClaudeClient::new(test_config(base_url)).expect("client config is valid"); + + let result = client + .create_message(vec![Message::user("hello")], None, EgressClass::UserText) + .await; + + assert!(result.is_ok(), "expected Ok, got {result:?}"); + assert_eq!( + calls.load(Ordering::SeqCst), + 1, + "an allowed request must reach the transport exactly once" + ); + } +} diff --git a/proofs/README.adoc b/proofs/README.adoc index fa607ac..1f3aae0 100644 --- a/proofs/README.adoc +++ b/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, 3.2 +| proptest | (in `crates/`) | executable evidence for 0.1, 0.2, 1.2, 1.3, 3.1 (veto enforcement), 3.2 | compile-fail tests| `neurophone-core` doc-tests | 2.1 (type level) + 2.3 release-once |=== @@ -45,7 +45,7 @@ by property tests over the operational paths; *open* = honest gap, never faked. | 2.1 | Lifecycle state-machine safety | *checked* — TLC on `tla/Lifecycle.{tla,cfg}` (no error; 13 states) + 3 compile-fail typestate doc-tests | 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.1 | Data-egress / privacy invariant | *property* — the `conative-gating` GO/NO-GO veto (#103) is now wired into `ClaudeClient::create_message`, the sole outbound-network choke point in `claude-client` (see `crates/claude-client/src/egress_gate.rs`); `egress_integration_tests::blocked_egress_never_reaches_the_network` proves a `Block` verdict results in *zero* network calls (against a real local fake-transport server) and `..._reaches_the_network_exactly_once` proves an allowed request is not obstructed. Honest gap: `EgressClass` is *caller-declared* (there is no independent sensor-provenance tracker yet), so a caller that mislabels raw data as derived/aggregated is not currently caught by this layer — see the module's doc comment for the exact boundary. Formal (non-property) proof remains open; no TLA+/Dafny spec for this obligation yet. | 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` |===