neurophone follow-up: JNI surface (#110), proofs, RSR, Trustfile, docs#156
Merged
Conversation
The standards governance staleness gate (governance-reusable @7c9db0e running
scripts/check-workflow-staleness.sh) hard-errors on this file:
::error:: scorecard-enforcer.yml is retired. Use scorecard.yml -> standards
scorecard-reusable.yml instead.
::error:: OSSF Scorecard must not upload SARIF to GitHub Code Scanning unless
it runs for every PR head commit.
The estate has retired the hand-rolled enforcer in favour of the canonical
scorecard.yml -> standards scorecard-reusable.yml path (which runs Scorecard in
JSON mode and uploads an artifact, without pushing per-push-only SARIF into
Code Scanning). Deleting the legacy file is how the running governance gate is
satisfied — solutions at source, not a local patch. scorecard.yml (re-pinned to
7c9db0e) remains as the canonical Scorecard runner.
Verified: check-workflow-staleness.sh now reports "All workflow staleness checks
passed" against standards HEAD.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh
Turns the 6-line stub into the full 11-method JNI boundary specified in
docs/migrations/JNI-SURFACE-AUDIT.adoc (class `ai.neurophone.NativeLib`),
gossamer-independent — gossamer changes who loads the cdylib, not this ABI.
crates/neurophone-android:
- lib.rs: 11 `#[unsafe(no_mangle)] extern "system"` exports (init, start,
stop, isRunning, processSensor, query, queryLocal, queryClaude,
getNeuralContext, getState, reset). Uses jni 0.22's safe `EnvUnowned::
with_env` + `resolve::<ThrowRuntimeExAndDefault>()`, so no unsafe *code*
(the crate is the sanctioned FFI boundary; the JNI export attribute is the
sole reason it can't `forbid(unsafe_code)`). Panics are caught by with_env
and never unwind across FFI.
- state.rs: the JVM-free bridge — `OnceLock<Mutex<Option<RuntimeState>>>`
holder + init/start/stop/process/query/reset. `reset` consumes the running
system through the core `shutdown(self)` typestate (Active -> Down, dropped
exactly once), wiring the resource-lifecycle property (#93/obligation 2.3)
through the boundary.
- sensor_map.rs: Android Sensor.TYPE_* id -> canonical name (moved out of the
former Kotlin shim per the audit).
- error.rs: JniBridgeError bridging jni + neurophone-core failures.
- Cargo.toml: crate-type ["lib","cdylib"] so host `cargo test` runs the
bridge tests; add thiserror; inherit license/authors/repository.
crates/neurophone-core:
- Add `QueryRoute` {Auto, ForceLocal, ForceCloud} + `query_routed` +
`select_model`; `query(msg, prefer_local)` now delegates, preserving the
historical contract exactly. `queryLocal`/`queryClaude` need this hard
routing that `prefer_local` alone cannot express.
- Add `get_neural_context()` composing the LLM-context string from real
SystemState fields (no invented salience).
Ground truth: cargo build/test OK (155 tests, +9), cargo clippy --all-targets
--workspace -- -D warnings clean, cargo fmt --check clean. Bridge logic is
host-tested (sensor map, full lifecycle, reset-preserves-state, bad-config).
Refs #110, #84 (2.3).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh
|
hyperpolymath
marked this pull request as ready for review
July 1, 2026 11:31
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
## 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>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Follow-up to the merged #154 (which landed the rand build-fix + CI re-pin). Continues
driving
neurophonetoward fully-proven / fully-engineered: issue disposition, QA +security, proofs, RSR compliance, the estate Trustfile, and docs. Draft — actively in
progress; this body tracks live state.
Landed so far
scorecard-enforcer.yml— the standards governance stalenessgate (
check-workflow-staleness.sh) hard-errors on this legacy file and on itsper-push-only SARIF upload to Code Scanning. The estate retired it in favour of
scorecard.yml→ standardsscorecard-reusable.yml. Deleting it is how the runninggate is satisfied (solutions at source). Verified: staleness check passes locally.
crates/neurophone-androidbecomes the full 11-methodai.neurophone.NativeLibboundary from
docs/migrations/JNI-SURFACE-AUDIT.adoc. jni 0.22 safeEnvUnowned::with_env(no unsafe code; panics caught at the boundary). Bridge logicis JVM-free and host-tested;
resetconsumes the coreshutdown(self)typestate(Active→Down, once), wiring the resource-lifecycle property. Adds
QueryRoute+query_routed+get_neural_contextto core (non-breaking;querydelegates).Gossamer-independent. Ground truth: 155 tests, clippy
-D warningsclean, fmt clean.In progress
Lifecycle.cfg+ TLC, trybuild use-after-shutdown, extend proptest;honest
proofs/README.adoc+spectral_radiusmisnomer note.descriptiles/, GOVERNANCE.adoc, k9 validators..claude/CLAUDE.md), STATE.a2ml, PMPL→MPL-2.0 correction.FLAGS — external / owner-plane (cannot resolve here)
gossamer+conative-gatingclones are 403-blocked by the egress policy, so thebuild: migrate Kotlin/Gradle Android app to gossamer (clears banned-language CI) #83 migration epic (build(#83): gossamer Android scaffolding (WebView host + JNI bridge) #109, build(#83): NeurophoneService → generated Java Service shim → JNI #111–build(#83): delete legacy android/ Kotlin+Gradle tree (both CI gates green) #115) and Adopt conative-gating as policy/egress GO/NO-GO veto (refs proof-obligation #84-3.1) #103 egress-veto are staged behind access
being granted at the platform level. Only the gossamer-independent build(#83): port NativeLib JNI to crates/neurophone-android (Rust) #110 proceeds.
HYPATIA_SCAN_PAT, Scorecard branch-protection/ code-review. If "OpenSSF Scorecard Enforcer" is still a required status check, its
context is now retired — please drop it from branch protection.
3.1 residual — honest, with completion paths; nothing faked.
🤖 Generated with Claude Code
https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh
Generated by Claude Code