diff --git a/docs/architecture.adoc b/docs/architecture.adoc new file mode 100644 index 0000000..c115841 --- /dev/null +++ b/docs/architecture.adoc @@ -0,0 +1,149 @@ +// SPDX-License-Identifier: MPL-2.0 += NeuroPhone Architecture +:toc: + +== Architecture + +=== Rust Crates (8 modules) + +|=== +| Crate | Purpose | Key Features + +| `lsm` +| Liquid State Machine +| 512 spiking neurons, 3D grid, 1kHz processing + +| `esn` +| Echo State Network +| 300-neuron reservoir, ridge regression + +| `bridge` +| Neural ↔ Symbolic +| State encoding, context generation + +| `sensors` +| Phone Sensors +| Accel, gyro, magnetometer, light, proximity + +| `llm` +| Local Inference +| Llama 3.2 via llama.cpp, streaming + +| `claude-client` +| Cloud Fallback +| Claude API, retry logic, context injection + +| `neurophone-core` +| Orchestration +| Main coordinator, query routing + +| `neurophone-android` +| Android JNI +| Kotlin ↔ Rust bridge +|=== + +=== Android App (Kotlin) + +``` +android/ +├── app/src/main/ +│ ├── java/ai/neurophone/ +│ │ ├── MainActivity.kt +│ │ ├── NativeLib.kt # JNI interface +│ │ ├── SensorManager.kt # Sensor collection +│ │ └── ui/ # Compose UI +│ └── res/ +└── build.gradle.kts +``` + +== Components + +=== LSM (Liquid State Machine) + +Spiking neural network for temporal sensor processing: + +* 3D grid: 8×8×8 = 512 Leaky Integrate-and-Fire neurons +* Distance-dependent connectivity +* Excitatory/inhibitory balance +* Real-time spike processing at 1kHz + +=== ESN (Echo State Network) + +Reservoir for state prediction: + +* 300-neuron reservoir +* Spectral radius: 0.95 +* Leaky integrator dynamics +* Ridge regression output + +=== Sensors + +Phone sensor integration: + +* Accelerometer, gyroscope, magnetometer +* Light and proximity sensors +* IIR filtering (low-pass, high-pass) +* Feature extraction at 50Hz + +=== Bridge + +Neural ↔ Symbolic translation: + +* Integrates LSM + ESN states +* Generates natural language context for LLMs +* Temporal pattern detection +* Salience and urgency computation + +=== Local LLM + +On-device language model: + +* Llama 3.2 1B/3B via llama.cpp +* Optimized for Dimensity 8350 +* Q4_K_M quantization (~700MB) +* Neural context injection + +=== Claude Client + +Cloud fallback for complex queries: + +* Messages API integration +* Automatic retry with exponential backoff +* Hybrid inference (local/cloud decision) +* Neural state context injection + +== Performance + +Optimized for Oppo Reno 13 (Dimensity 8350): + +|=== +| Component | Latency | Notes + +| Sensor processing +| <1ms +| 50Hz loop + +| LSM step +| <2ms +| 512 neurons + +| ESN step +| <1ms +| 300 neurons + +| Bridge integration +| <1ms +| Per step + +| Local LLM (1B) +| 50-100ms/token +| Q4 quantized + +| Claude API +| 500-2000ms +| Network dependent +|=== + +== Topology + +See link:../TOPOLOGY.md[TOPOLOGY.md] for a visual architecture map and completion dashboard. diff --git a/docs/build.adoc b/docs/build.adoc new file mode 100644 index 0000000..5fa6c39 --- /dev/null +++ b/docs/build.adoc @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: MPL-2.0 += Building NeuroPhone +:toc: + +== Getting Started + +=== Prerequisites + +* Rust 1.75+ +* Android NDK 26+ +* Android Studio (for app development) +* Oppo Reno 13 or Android 8.0+ device + +=== Build + +```bash +# Clone +git clone https://github.com/hyperpolymath/neurophone +cd neurophone + +# Setup +./scripts/setup.sh + +# Build native libraries for Android +./scripts/build-android.sh + +# Open android/ in Android Studio +``` + +=== Download LLM Model + +```bash +# Download Llama 3.2 1B Instruct (Q4_K_M, ~700MB) +# From: https://huggingface.co/bartowski/Llama-3.2-1B-Instruct-GGUF + +# Push to device +adb push llama-3.2-1b-instruct-q4_k_m.gguf /data/local/tmp/ +``` + +=== Configure + +Set Claude API key (for cloud fallback): + +```bash +export ANTHROPIC_API_KEY="your-api-key" +``` + +Or in `config/default.toml`: + +```toml +[claude] +api_key = "your-api-key" +model = "claude-sonnet-4-20250514" + +[llm] +model_path = "/data/local/tmp/llama-3.2-1b-q4_k_m.gguf" +n_threads = 4 +context_size = 2048 +``` + +== Development + +```bash +# Run tests +cargo test + +# Build for Android +./scripts/build-android.sh + +# Generate docs +cargo doc --open +``` diff --git a/docs/installation.adoc b/docs/installation.adoc new file mode 100644 index 0000000..4b623a2 --- /dev/null +++ b/docs/installation.adoc @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: MPL-2.0 += Installing NeuroPhone +:toc: + +[[ai-install]] +== AI-Assisted Installation (Recommended) + +=== Just Say It + +**You don't need to read this README.** Just say this to any AI assistant: + +[source,text] +---- +Set up NeuroPhone on my Android from https://github.com/hyperpolymath/neurophone +---- + +**That's it. You don't type commands, install packages, or configure anything.** The AI fetches this repo, reads the installation guide inside it, figures out your device, and does everything. You just answer a few questions and confirm the privacy notice. + +The URL is the key -- it points the AI to this repo where `docs/AI_INSTALLATION_GUIDE.adoc` contains the complete step-by-step recipe. Any AI that can read a URL and run commands (or generate commands for you to paste) can do this. + +The AI handles all of this automatically: + +* Checking your device and storage +* Installing Termux (if needed), Rust, Git, and dependencies +* Cloning and building NeuroPhone for your specific hardware +* Downloading the right LLM model for your device's RAM/storage +* Creating your configuration with sensible defaults +* Running the setup wizard +* Giving you a working NeuroPhone + +=== Other Ways to Say It + +If your AI already knows about NeuroPhone (e.g. it can search the web), even shorter versions work: + +* "Make my phone a NeuroPhone" +* "Install NeuroPhone on my Android" +* "Turn my Oppo Reno 13 into a NeuroPhone" + +If it doesn't know the project, just include the URL: + +* "Set up https://github.com/hyperpolymath/neurophone on my phone" +* "I want neurosymbolic AI on my phone -- install from https://github.com/hyperpolymath/neurophone" + +=== What You'll Be Asked + +Your AI will ask you: + +1. **What device?** (so it picks the right thread count and model size) +2. **Privacy confirmation** -- what sensors are used and how data stays on-device +3. **Cloud fallback?** (optional Claude API for complex queries -- default is local-only) + +That's it. Everything else is automatic. No package managers, no build flags, no config files. + +=== Privacy & Security Notice + +[IMPORTANT] +==== +**What NeuroPhone does:** + +* Reads phone sensors (accelerometer, gyroscope, magnetometer, light, proximity) +* Processes everything on-device using Rust neural networks + local Llama LLM +* Stores neural states locally in `~/.local/share/neurophone/` (never uploaded) +* Optionally uses Claude API for complex queries (you control this) + +**What NeuroPhone does NOT do:** + +* Upload sensor data to any server (unless you enable cloud fallback) +* Track you or collect analytics +* Access camera, microphone, contacts, or personal data + +**You control everything:** cloud fallback toggle, all config in `~/.config/neurophone/`, uninstall anytime. +==== + +=== After Install + +Once your AI finishes setup, just use it: + +[source,bash] +---- +neurophone # Start NeuroPhone +neurophone query "What am I doing right now?" # Ask a question +neurophone status # Check system status +---- + +=== Uninstall + +Tell your AI: "Uninstall NeuroPhone from my phone" + +=== Troubleshooting + +Tell your AI what went wrong -- it can read the troubleshooting docs in this repo. Common issues: + +[cols="1,3"] +|=== +|Problem |Solution + +|"Termux not found" +|AI will guide you to install from F-Droid (NOT Google Play) + +|Build takes too long +|Normal for first build (5-10 min). AI adjusts thread count for your device. + +|"Model download failed" +|AI will try alternate download methods or suggest `adb push` from PC + +|"LSM crashes" +|Low RAM. AI will reduce model size or neuron count for your device. +|=== + +[[manual-installation]] +For manual installation without AI assistance, see link:build.adoc[Building NeuroPhone]. + +See also the complete machine-readable recipe in link:AI_INSTALLATION_GUIDE.adoc[AI_INSTALLATION_GUIDE.adoc]. diff --git a/docs/usage.adoc b/docs/usage.adoc new file mode 100644 index 0000000..a6bba41 --- /dev/null +++ b/docs/usage.adoc @@ -0,0 +1,41 @@ +// SPDX-License-Identifier: MPL-2.0 += NeuroPhone Usage +:toc: + +== Usage + +=== Kotlin API + +```kotlin +// Initialize +NativeLib.init() +NativeLib.start() + +// Query with neural context +val response = NativeLib.query("What's my current activity?", preferLocal = true) + +// Get raw neural state +val context = NativeLib.getNeuralContext() +// Returns: [NEURAL_STATE] Description: ... [/NEURAL_STATE] + +// Cleanup +NativeLib.stop() +``` + +=== Rust API + +```rust +use neurophone_core::{NeuroSymbolicSystem, SystemConfig}; + +let mut system = NeuroSymbolicSystem::with_config(config)?; +let _rx = system.start().await?; + +// Send sensor data +system.send_sensor(reading).await?; + +// Query +let response = system.query("What's happening?", true).await?; + +// Get neural context +let context = system.get_neural_context().await; +``` diff --git a/proofs/README.adoc b/proofs/README.adoc new file mode 100644 index 0000000..28620db --- /dev/null +++ b/proofs/README.adoc @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: MPL-2.0 += NeuroPhone Proof Corpus +:toc: + +This directory holds the formal-verification artefacts for neurophone. It exists +so the obligations declared in `.machine_readable/MUST.contractile` +("no removal of formal verification proofs", "no ABI change without proof +update", and the bans on `Admitted`/`sorry`/`believe_me`/`Obj.magic`) refer to a +real corpus rather than being vacuous. + +The full obligation map and its rationale live in +https://github.com/hyperpolymath/neurophone/issues/84[issue #84]. This README is +the index from each obligation to the artefact that discharges it. + +== Toolchain split + +[cols="1,2,2",options="header"] +|=== +| Tool | Directory | Obligations +| TLA+ (TLC) | `proofs/tla/` | 2.1 lifecycle, 2.2 concurrency, 3.1 data egress +| Lean / Coq | `proofs/lean/` | 1.1 echo state property, 1.3 bridge soundness +| Dafny / F* | `proofs/dafny/` | 1.2 LSM bounded dynamics, 0.2 numeric containment +| Kani + proptest | (in `crates/`) | executable bridge from spec to Rust (0.1, 0.2, 1.2) +|=== + +== Status + +[cols="1,3,1",options="header"] +|=== +| ID | Obligation | State +| 0.1 | Panic-freedom on operational paths | open +| 0.2 | Numeric containment (no NaN/Inf, no overflow) | open +| 0.3 | `unsafe` discipline (`deny`/`forbid` all crates) | *done* +| 1.1 | Echo State Property (reservoir is a contraction)| spec: `tla/`+`lean/` (open) +| 1.2 | LSM bounded dynamics | open +| 1.3 | Bridge soundness (neural→symbolic) | open +| 2.1 | Lifecycle state-machine safety | spec: `tla/Lifecycle.tla` +| 2.2 | Concurrency safety (no deadlock) | open +| 2.3 | Resource/affine lifecycle | open +| 3.1 | Data-egress / privacy invariant | open +| 3.2 | Bounded external interaction | open +|=== + +== Ground rules + +* No proof escape hatches (`Admitted`, `sorry`, `believe_me`, `assert_total`, + `Obj.magic`, `unsafeCoerce`) — enforced by `MUST.contractile`. An obligation + is either fully discharged or left as a spec/`open`; never faked. +* `unsafe` discipline (0.3): `sensors`, `bridge`, `neurophone-core`, + `claude-client`, `llm` use `#![forbid(unsafe_code)]`. `esn` and `lsm` use + `#![deny(unsafe_code)]` instead of `forbid` because they invoke macros + (`ndarray-rand` / `rand_distr`) that expand to an inner `#[allow(unsafe_code)]`, + which `forbid` — uniquely — rejects (E0453). `deny` still makes any unsafe we + write a hard error unless explicitly allowed with a safety comment (per MUST). +* Each artefact carries an SPDX header and a comment linking back to its + obligation ID and issue #84. diff --git a/proofs/dafny/README.adoc b/proofs/dafny/README.adoc new file mode 100644 index 0000000..699a9a9 --- /dev/null +++ b/proofs/dafny/README.adoc @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: MPL-2.0 += Dafny / F* proofs + +Obligations discharged here (see issue #84): + +* *1.2 LSM bounded dynamics* — the discretised Leaky Integrate-and-Fire update + keeps the membrane potential within `[reset, threshold + ε]`, respects the + refractory period, bounds the firing rate given bounded input, and keeps the + spike-history ring buffers within capacity. +* *0.2 Numeric containment* — the sensor and reservoir kernels neither produce + nor propagate NaN/Inf, and integer indexing/accumulation does not overflow. + +Models are written against the algorithm; the Rust implementation is tied back +to them with Kani harnesses and `proptest` properties in the respective crates. diff --git a/proofs/lean/README.adoc b/proofs/lean/README.adoc new file mode 100644 index 0000000..2f2de9b --- /dev/null +++ b/proofs/lean/README.adoc @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: MPL-2.0 += Lean / Coq proofs + +Obligations discharged here (see issue #84): + +* *1.1 Echo State Property* — the ESN update map + `x' = (1-a)·x + a·tanh(W·x + W_in·u)` is a contraction whenever the + recurrent matrix satisfies `‖W‖∞ < 1` (the sufficient condition the code + currently enforces via `scale_to_spectral_radius`). tanh is 1-Lipschitz and + the leaking-rate convex combination is non-expansive, so the composite map is + a contraction in the ∞-norm ⇒ the Echo State (fading-memory) Property holds. +* *1.3 Bridge soundness* — the neural→symbolic encoding in `crates/bridge` is + total and deterministic, and round-trips within tolerance. + +No `sorry` / `admit` is permitted (enforced by `MUST.contractile`); a file lands +here only when its theorems are fully proved. diff --git a/proofs/tla/Lifecycle.tla b/proofs/tla/Lifecycle.tla new file mode 100644 index 0000000..c580bd1 --- /dev/null +++ b/proofs/tla/Lifecycle.tla @@ -0,0 +1,55 @@ +---------------------------- MODULE Lifecycle ---------------------------- +(* SPDX-License-Identifier: MPL-2.0 *) +(* Obligation 2.1 (issue #84): lifecycle safety for *) +(* neurophone-core::NeuroSymbolicSystem. *) +(* *) +(* Models the intended protocol: *) +(* new -> initialize -> { process_sensor_event | query }* -> shutdown *) +(* *) +(* Safety claims (checked by TLC against this spec): *) +(* - no process/query before initialize *) +(* - no action after shutdown (shutdown is terminal & idempotent) *) +(*========================================================================*) +EXTENDS Naturals + +VARIABLES + phase, \* "created" | "initialized" | "down" + work \* count of process/query operations performed + +vars == <> + +TypeOK == /\ phase \in {"created", "initialized", "down"} + /\ work \in Nat + +Init == /\ phase = "created" + /\ work = 0 + +Initialize == /\ phase = "created" + /\ phase' = "initialized" + /\ UNCHANGED work + +ProcessOrQuery == /\ phase = "initialized" + /\ phase' = "initialized" + /\ work' = work + 1 + +Shutdown == /\ phase = "initialized" + /\ phase' = "down" + /\ UNCHANGED work + +\* No transition is enabled from "down": shutdown is terminal & idempotent. +Next == \/ Initialize + \/ ProcessOrQuery + \/ Shutdown + +Spec == Init /\ [][Next]_vars + +(* ---- Safety invariants ---- *) + +\* Any work that happened implies we are at or past initialization. +NoUseBeforeInit == (work > 0) => (phase \in {"initialized", "down"}) + +\* Once down, we never perform more work and never leave "down". +NoUseAfterShutdown == [][ (phase = "down") => (phase' = "down" /\ work' = work) ]_vars + +THEOREM Spec => [](TypeOK /\ NoUseBeforeInit) +==========================================================================