neurophone: proofs (2.1 TLC / 2.3 typestate) + estate Trustfile#158
Merged
Conversation
…tus map Advances the proof-obligation map (#84) along the honest staged path — every claim below is backed by a checker or property run this session; nothing faked (MUST forbids sorry/Admitted/believe_me). - 2.1 lifecycle: add proofs/tla/Lifecycle.cfg + WorkBound so TLC can model-check proofs/tla/Lifecycle.tla. TLC now reports "No error has been found" (13 states): TypeOK, NoUseBeforeInit invariants and the NoUseAfterShutdown temporal property all hold. CHECK_DEADLOCK FALSE because "down" is intentionally terminal. - 2.1 (type level) + 2.3 release-once: three compile-fail doc-tests on NeuroSymbolicSystem prove the typestate rejects use-before-init, use-after-shutdown, and double-shutdown (shutdown consumes self). `cargo test` fails if any ever starts compiling. - 0.1 panic-freedom + 0.2 numeric containment on the core operational paths: crates/neurophone-core/tests/proptest_core.rs — process_sensor_event / query never panic and stay contained (finite features, length-preserving, confidence in [0,1]) over arbitrary finite inputs and all routing modes. - proofs/README.adoc: rewritten to reflect reality (0.1/0.2/1.2/1.3 property- discharged, 2.1 TLC-checked, 2.3 compile-fail-verified; 1.1/2.2/3.1/3.2 honest OPEN with completion paths). Corrects the stale "open" markings. Records that the earlier spectral_radius misnomer is already FIXED in esn (power-iteration estimate + scale), so 1.1's precondition holds and only the formal contraction proof remains. - Justfile: `proof-tla` (fetches tla2tools.jar to .tlacache/, self-skips without java), `proof` (cargo test + TLC), and the RSR `quality` gate. .gitignore the jar cache. Ground truth: cargo test 160 pass (+5), clippy --all-targets -- -D warnings clean, fmt clean; TLC verified locally. Refs #84 (0.1, 0.2, 2.1, 2.3), #93. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh
Replaces the 23-line minimal Trustfile with the full estate baseline
(A2ML Trustfile v2026.2.5-final), specialised for neurophone.
.machine_readable/contractiles/trust/Trustfile.a2ml (canonical):
- META (DID did:web:github.com:hyperpolymath:neurophone, hybrid-sig block),
THREAT_MODEL (on-device app: malicious JNI caller, MITM on the Claude
fallback, model extraction, sensor spoofing, supply chain, quantum — each
mitigation grounded in a real property: typestate lifecycle, forbid(unsafe),
numeric-containment proptests, egress confinement), TRUSTFILE
(issuer/keys/algorithms + egress-default-deny / FFI-delegation / secrets /
totality policies), ESTATE_STANDARD, REPOSITORY_SPECIFIC (architecture +
runnable trust-deny / no-secrets / license-content checks), PROOF_ARTIFACTS
(the honest 0.1-3.2 map: 2.1 PROVEN via TLC, 2.3 PROVEN via compile-fail,
0.1/0.2/1.2/1.3 TESTED, 1.1/2.2/3.1/3.2 DESIGNED, with open_obligations +
explicit non_claims), CI_CD, AUTOMATION, CAPABILITY_GATEWAY, SSL/TLS (Claude
egress only), CRYPTO_AGILITY, TRANSPARENCY_LOG, PLACEHOLDER_TRACKING,
NOT_APPLICABLE (DNS/email/Cloudflare/PHP — no web surface), SIGNATURE_BLOCK,
DEPLOYMENT.
- Crypto material (Ed448+Dilithium5 / SPHINCS+ signatures, public JWKs,
integrity hashes, transparency entries) left as {{PLACEHOLDER}} — owner
fills these at signing time; never fabricated.
contractiles/trust/Trustfile.a2ml: keep the fast k9-style checks, point to the
canonical file, tighten license-content to MPL-2.0 (drop the stale PMPL grep).
.github/workflows/trustfile.yml (new, SHA-pinned, least-privilege): structural
section lint, placeholder policy (WARN on branches / ERROR on main so
owner-pending crypto doesn't red the draft), integrity-hash drift report (no
auto-commit on protected branch), and the runnable integrity checks.
Verified locally: YAML valid, all required sections present, license/no-secrets
checks pass, checkout pin matches the repo's existing v4.2.2 pin.
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:45
|
hyperpolymath
added a commit
that referenced
this pull request
Jul 1, 2026
…OVERNANCE.adoc (#160) ## Summary Documentation-correctness + RSR-compliance follow-up (after merged #158). - **chore(licence): PMPL-1.0 → MPL-2.0 drift correction (owner-approved).** neurophone is a sole-owner MPL-2.0 repo (licence reverted from PMPL in #102/#118 per HANDOVER), but several *functional* declarations still read PMPL. Corrected README badge/body, `META.a2ml`/`stapeln.toml` licence fields, `AGENTIC.a2ml`, `0-AI-MANIFEST.a2ml`, `QUICKSTART-MAINTAINER.adoc`, `llm-warmup-{dev,user}.md`. **Deliberately not touched** (owner territory): `PALIMPSEST.adoc`, `docs/CITATIONS.adoc`, `docs/governance/*`, `LICENSES/*.txt`, and the README Palimpsest-*philosophy* badge. Docs stay CC-BY-SA-4.0. - **docs: refresh stale `.claude/CLAUDE.md` language policy** — drop the removed Python/SaltStack allowance and the Nix fallback (Guix-only); Rust→Rust/SPARK; add Zig/Idris2; add ReScript/V-lang/ATS2/Nix/Makefiles to BANNED. - **docs: correct `STATE.a2ml`** — the neural crates were mislabelled "stub" but carry real code + property suites; neurophone-android is now the full JNI surface. Records 160 tests, clippy/fmt/TLC clean, a `[proofs]` block, and honest external `[blockers]`. - **docs: dedup CONTRIBUTING** — removed the 402-byte `.adoc` stub (estate keeps the GitHub-required `.md`; nothing referenced the `.adoc`). - **docs(rsr): add `GOVERNANCE.adoc`** (was missing at root) and mark the JNI surface audit as implemented by #110. No code changes; docs/config only. (Prior branch verification stands: 160 tests, clippy `-D warnings` clean, fmt clean.) ## FLAGS (unchanged) - `gossamer` + `conative-gating` remain 403-blocked → #83 / #103 staged. - 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
Continues the neurophone hardening (follow-up to the merged #154, #156). Two chunks:
Proofs — honest staged path (#84)
proofs/tla/Lifecycle.cfg+ aWorkBoundconstraint; TLC now reports "No error has been found" (13 states) —TypeOK,NoUseBeforeInit, and theNoUseAfterShutdownproperty all hold.compile_faildoc-tests on
NeuroSymbolicSystemprove the typestate rejects use-before-init,use-after-shutdown, and double-shutdown —
cargo testfails if any starts compiling.neurophone-core/tests/proptest_core.rs.proofs/README.adocrewritten to reflect reality (property/checked/open), andcorrected: the
spectral_radiusmisnomer is already fixed inesn(poweriteration), so 1.1's precondition holds — only the formal contraction proof remains.
Justfile:proof-tla(fetchestla2tools.jar, self-skips without java),proof,and the RSR
qualitygate.Estate Trustfile (owner's explicit ask)
.machine_readable/contractiles/trust/Trustfile.a2mlupgraded from 23 lines to thefull 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_ARTIFACTSmap withexplicit
non_claims, capability gateway, crypto-agility. Owner-only crypto(Ed448+Dilithium5 / SPHINCS+, hashes, transparency entries) left as
{{PLACEHOLDER}}..github/workflows/trustfile.ymlgate: structural lint + placeholderpolicy (WARN on branches / ERROR on main) + integrity-hash drift report + runnable checks.
Ground truth:
cargo test160 pass,cargo clippy --all-targets -- -D warningsclean,
cargo fmt --checkclean; TLC verified locally.FLAGS — external / owner-plane (unchanged)
gossamer+conative-gatingclones remain 403-blocked → build: migrate Kotlin/Gradle Android app to gossamer (clears banned-language CI) #83 epic and Adopt conative-gating as policy/egress GO/NO-GO veto (refs proof-obligation #84-3.1) #103 staged.{{PLACEHOLDER}}crypto at signing time.🤖 Generated with Claude Code
https://claude.ai/code/session_0172RBMz3qYjb1ttzD2i7RNh
Generated by Claude Code