diff --git a/.github/workflows/cargo-audit.yml b/.github/workflows/cargo-audit.yml index ca42f96..ae3236d 100644 --- a/.github/workflows/cargo-audit.yml +++ b/.github/workflows/cargo-audit.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: PMPL-1.0-or-later # Prevention workflow - audits Rust dependencies for vulnerabilities name: Cargo Audit diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 1d6417e..29f6f39 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: PMPL-1.0-or-later # Thin wrapper around hyperpolymath/standards hypatia-scan-reusable.yml. # See standards#191 for the reusable's purpose and design. diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 9ab8801..983c6d2 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: PMPL-1.0-or-later # Rust CI — thin wrapper calling the shared estate reusable in # hyperpolymath/standards. Configure once, propagate everywhere. # See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards. diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 02b2e76..b5ba94d 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: MPL-2.0 +# SPDX-License-Identifier: PMPL-1.0-or-later # Prevention workflow - validates all workflows have proper security config name: Workflow Security Linter diff --git a/0-AI-MANIFEST.a2ml b/0-AI-MANIFEST.a2ml index aadb4cf..b29e53f 100644 --- a/0-AI-MANIFEST.a2ml +++ b/0-AI-MANIFEST.a2ml @@ -43,7 +43,7 @@ Bot-specific instructions for: 1. **No SCM duplication** - Root must NOT contain .machine_readable/6a2/STATE.a2ml, .machine_readable/6a2/META.a2ml, etc. 2. **Single source of truth** - `.machine_readable/` is authoritative 3. **No stale metadata** - If root SCMs exist, they are OUT OF DATE -4. **License consistency** - All code PMPL-1.0-or-later unless platform requires MPL-2.0 +4. **License consistency** - All code PMPL-1.0-or-later 5. **Author attribution** - Always "Jonathan D.A. Jewell " ## REPOSITORY STRUCTURE diff --git a/CHANGELOG.md b/CHANGELOG.md index 2b432c7..94741e4 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,5 @@ diff --git a/CONTRIBUTING.adoc b/CONTRIBUTING.adoc index a0f2f54..c73e96f 100644 --- a/CONTRIBUTING.adoc +++ b/CONTRIBUTING.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0-or-later +// SPDX-License-Identifier: PMPL-1.0-or-later = Contributing Guide == Getting Started diff --git a/Cargo.lock b/Cargo.lock index c6f4eec..8ebfe5e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -144,7 +144,7 @@ dependencies = [ "ndarray", "ndarray-rand", "proptest", - "rand 0.10.1", + "rand", "serde", "serde_json", "thiserror 2.0.18", @@ -199,17 +199,6 @@ version = "0.2.1" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" -[[package]] -name = "chacha20" -version = "0.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6f8d983286843e49675a4b7a2d174efe136dc93a18d69130dd18198a6c167601" -dependencies = [ - "cfg-if", - "cpufeatures", - "rand_core 0.10.1", -] - [[package]] name = "chrono" version = "0.4.44" @@ -327,15 +316,6 @@ version = "0.8.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" -[[package]] -name = "cpufeatures" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b2a41393f66f16b0823bb79094d54ac5fbd34ab292ddafb9a0456ac9f87d201" -dependencies = [ - "libc", -] - [[package]] name = "criterion" version = "0.8.2" @@ -460,8 +440,8 @@ dependencies = [ "ndarray", "ndarray-rand", "proptest", - "rand 0.10.1", - "rand_distr 0.6.0", + "rand", + "rand_distr", "rayon", "serde", "thiserror 2.0.18", @@ -631,7 +611,6 @@ dependencies = [ "cfg-if", "libc", "r-efi 6.0.0", - "rand_core 0.10.1", "wasip2", "wasip3", ] @@ -1118,8 +1097,8 @@ dependencies = [ "criterion", "ndarray", "ndarray-rand", - "rand 0.10.1", - "rand_distr 0.6.0", + "rand", + "rand_distr", "rayon", "serde", "thiserror 2.0.18", @@ -1186,8 +1165,8 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "180f724d496e84764e8ecf28fbe1da74ef231ec4ba15be65a9100be8445d73e3" dependencies = [ "ndarray", - "rand 0.9.4", - "rand_distr 0.5.1", + "rand", + "rand_distr", ] [[package]] @@ -1420,7 +1399,7 @@ dependencies = [ "bit-vec", "bitflags", "num-traits", - "rand 0.9.4", + "rand", "rand_chacha", "rand_xorshift", "regex-syntax", @@ -1465,7 +1444,7 @@ dependencies = [ "bytes", "getrandom 0.3.4", "lru-slab", - "rand 0.9.4", + "rand", "ring", "rustc-hash", "rustls", @@ -1519,18 +1498,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "44c5af06bb1b7d3216d91932aed5265164bf384dc89cd6ba05cf59a35f5f76ea" dependencies = [ "rand_chacha", - "rand_core 0.9.5", -] - -[[package]] -name = "rand" -version = "0.10.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d2e8e8bcc7961af1fdac401278c6a831614941f6164ee3bf4ce61b7edb162207" -dependencies = [ - "chacha20", - "getrandom 0.4.2", - "rand_core 0.10.1", + "rand_core", ] [[package]] @@ -1540,7 +1508,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "d3022b5f1df60f26e1ffddd6c66e8aa15de382ae63b3a0c1bfc0e4d3e3f325cb" dependencies = [ "ppv-lite86", - "rand_core 0.9.5", + "rand_core", ] [[package]] @@ -1552,12 +1520,6 @@ dependencies = [ "getrandom 0.3.4", ] -[[package]] -name = "rand_core" -version = "0.10.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "63b8176103e19a2643978565ca18b50549f6101881c443590420e4dc998a3c69" - [[package]] name = "rand_distr" version = "0.5.1" @@ -1565,17 +1527,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "6a8615d50dcf34fa31f7ab52692afec947c4dd0ab803cc87cb3b0b4570ff7463" dependencies = [ "num-traits", - "rand 0.9.4", -] - -[[package]] -name = "rand_distr" -version = "0.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4d431c2703ccf129de4d45253c03f49ebb22b97d6ad79ee3ecfc7e3f4862c1d8" -dependencies = [ - "num-traits", - "rand 0.10.1", + "rand", ] [[package]] @@ -1584,7 +1536,7 @@ version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "513962919efc330f829edb2535844d1b912b0fbe2ca165d613e4e8788bb05a5a" dependencies = [ - "rand_core 0.9.5", + "rand_core", ] [[package]] diff --git a/Cargo.toml b/Cargo.toml index 0ab7d55..eaed48a 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -14,7 +14,7 @@ members = [ [workspace.package] version = "1.0.0" edition = "2021" -license = "MPL-2.0" +license = "PMPL-1.0-or-later" authors = ["Jonathan D.A. Jewell "] repository = "https://github.com/hyperpolymath/neurophone" @@ -22,8 +22,8 @@ repository = "https://github.com/hyperpolymath/neurophone" # Core neural network ndarray = { version = "0.17", features = ["rayon", "serde"] } ndarray-rand = "0.16" -rand = "0.10" -rand_distr = "0.6" +rand = "0.9" +rand_distr = "0.5" rayon = "1.12" # Serialization diff --git a/LICENSE b/LICENSE index 2a8b960..f639385 100644 --- a/LICENSE +++ b/LICENSE @@ -1,375 +1,162 @@ -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: PMPL-1.0-or-later +SPDX-FileCopyrightText: 2025 Palimpsest Stewardship Council + +================================================================================ +PALIMPSEST-MPL LICENSE VERSION 1.0 +================================================================================ -Mozilla Public License Version 2.0 -================================== +File-level copyleft with ethical use and quantum-safe provenance + +Based on Mozilla Public License 2.0 -1. Definitions --------------- +-------------------------------------------------------------------------------- +PREAMBLE +-------------------------------------------------------------------------------- -1.1. "Contributor" - means each individual or legal entity that creates, contributes to - the creation of, or owns Covered Software. +This License extends the Mozilla Public License 2.0 (MPL-2.0) with provisions +for ethical use, post-quantum cryptographic provenance, and emotional lineage +protection. The base MPL-2.0 terms apply except where explicitly modified by +the Exhibits below. + +Like a palimpsest manuscript where each layer builds upon what came before, +this license recognizes that creative works carry history, context, and meaning +that transcend mere code or text. + +-------------------------------------------------------------------------------- +SECTION 1: BASE LICENSE +-------------------------------------------------------------------------------- + +This License incorporates the full text of Mozilla Public License 2.0 by +reference. The complete MPL-2.0 text is available at: +https://www.mozilla.org/en-US/MPL/2.0/ + +All terms, conditions, and definitions from MPL-2.0 apply except where +explicitly modified by the Exhibits in this License. -1.2. "Contributor Version" - means the combination of the Contributions of others (if any) used - by a Contributor and that particular Contributor's Contribution. +-------------------------------------------------------------------------------- +SECTION 2: ADDITIONAL DEFINITIONS +-------------------------------------------------------------------------------- -1.3. "Contribution" - means Covered Software of a particular Contributor. +2.1. "Emotional Lineage" + means the narrative, cultural, symbolic, and contextual meaning embedded + in Covered Software, including but not limited to: protest traditions, + cultural heritage, trauma narratives, and community stories. + +2.2. "Provenance Metadata" + means cryptographically signed attribution information attached to or + associated with Covered Software, including author identities, timestamps, + modification history, and lineage references. + +2.3. "Non-Interpretive System" + means any automated system that processes Covered Software without + preserving or considering its Emotional Lineage, including but not + limited to: AI training pipelines, content aggregators, and automated + summarization tools. -1.4. "Covered Software" - means Source Code Form to which the initial Contributor has attached - the notice in Exhibit A, the Executable Form of such Source Code - Form, and Modifications of such Source Code Form, in each case - including portions thereof. +2.4. "Quantum-Safe Signature" + means a cryptographic signature using algorithms resistant to attacks + by quantum computers, as specified in Exhibit B. -1.5. "Incompatible With Secondary Licenses" - means +-------------------------------------------------------------------------------- +SECTION 3: ETHICAL USE REQUIREMENTS +-------------------------------------------------------------------------------- - (a) that the initial Contributor has attached the notice described - in Exhibit B to the Covered Software; or +In addition to the rights and obligations under MPL-2.0: - (b) that the Covered Software was made available under the terms of - version 1.1 or earlier of the License, but not also under the - terms of a Secondary License. +3.1. Emotional Lineage Preservation + You must make reasonable efforts to preserve and communicate the + Emotional Lineage of Covered Software when distributing or creating + derivative works. This includes maintaining narrative context, cultural + attributions, and symbolic meaning where documented. -1.6. "Executable Form" - means any form of the work other than Source Code Form. +3.2. Non-Interpretive System Notice + If You use Covered Software as input to a Non-Interpretive System, You + must: + (a) document such use in a publicly accessible manner; and + (b) not claim that outputs of such systems carry the Emotional Lineage + of the original work without explicit permission from Contributors. -1.7. "Larger Work" - means a work that combines Covered Software with other material, in - a separate file or files, that is not Covered Software. +3.3. Ethical Use Declaration + Commercial use of Covered Software requires acknowledgment that You have + read and understood Exhibit A (Ethical Use Guidelines) and agree to act + in good faith accordance with its principles. -1.8. "License" - means this document. +See Exhibit A for complete Ethical Use Guidelines. -1.9. "Licensable" - means having the right to grant, to the maximum extent possible, - whether at the time of the initial grant or subsequently, any and - all of the rights conveyed by this License. +-------------------------------------------------------------------------------- +SECTION 4: PROVENANCE REQUIREMENTS +-------------------------------------------------------------------------------- -1.10. "Modifications" - means any of the following: +4.1. Metadata Preservation + You must not strip, alter, or obscure Provenance Metadata from Covered + Software except where technically necessary and with clear documentation + of any changes. - (a) any file in Source Code Form that results from an addition to, - deletion from, or modification of the contents of Covered - Software; or +4.2. Quantum-Safe Provenance (Optional) + Contributors may sign their Contributions using Quantum-Safe Signatures. + If Quantum-Safe Signatures are present, You must preserve them in all + distributions. - (b) any new file in Source Code Form that contains any Covered - Software. +4.3. Lineage Chain + When creating derivative works, You should extend the provenance chain + to include Your own contributions, maintaining cryptographic linkage to + prior Contributors where feasible. -1.11. "Patent Claims" of a Contributor - means any patent claim(s), including without limitation, method, - process, and apparatus claims, in any patent Licensable by such - Contributor that would be infringed, but for the grant of the - License, by the making, using, selling, offering for sale, having - made, import, or transfer of either its Contributions or its - Contributor Version. +See Exhibit B for Quantum-Safe Provenance specifications. -1.12. "Secondary License" - means either the GNU General Public License, Version 2.0, the GNU - Lesser General Public License, Version 2.1, the GNU Affero General - Public License, Version 3.0, or any later versions of those - licenses. +-------------------------------------------------------------------------------- +SECTION 5: GOVERNANCE +-------------------------------------------------------------------------------- + +5.1. Stewardship Council + This License is maintained by the Palimpsest Stewardship Council, which + may issue clarifications, interpretive guidance, and future versions. + +5.2. Version Selection + You may use Covered Software under this version of the License or any + later version published by the Palimpsest Stewardship Council. + +5.3. Dispute Resolution + Disputes regarding interpretation of Ethical Use Requirements (Section 3) + should first be submitted to the Palimpsest Stewardship Council for + non-binding guidance before pursuing legal remedies. + +-------------------------------------------------------------------------------- +SECTION 6: COMPATIBILITY +-------------------------------------------------------------------------------- + +6.1. MPL-2.0 Compatibility + Covered Software under this License may be combined with software under + MPL-2.0. The combined work must comply with both licenses. + +6.2. Secondary Licenses + The Secondary License provisions of MPL-2.0 Section 3.3 apply to this + License. + +-------------------------------------------------------------------------------- +EXHIBITS +-------------------------------------------------------------------------------- + +Exhibit A - Ethical Use Guidelines +Exhibit B - Quantum-Safe Provenance Specification + +See separate files: +- EXHIBIT-A-ETHICAL-USE.txt +- EXHIBIT-B-QUANTUM-SAFE.txt + +-------------------------------------------------------------------------------- +END OF PALIMPSEST-MPL-1.0 LICENSE TEXT +-------------------------------------------------------------------------------- + +For exhibits, specifications, provenance rules, and governance: +https://github.com/hyperpolymath/palimpsest-license -1.13. "Source Code Form" - means the form of the work preferred for making modifications. +For legal frameworks and jurisdictional analysis: +See /legal/frameworks/ -1.14. "You" (or "Your") - means an individual or a legal entity exercising rights under this - License. For legal entities, "You" includes any entity that - controls, is controlled by, or is under common control with You. For - purposes of this definition, "control" means (a) the power, direct - or indirect, to cause the direction or management of such entity, - whether by contract or otherwise, or (b) ownership of more than - fifty percent (50%) of the outstanding shares or beneficial - ownership of such entity. +For provenance and audit tooling: +See /tools/ and /spec/PROVENANCE-SPEC.adoc -2. License Grants and Conditions --------------------------------- - -2.1. Grants - -Each Contributor hereby grants You a world-wide, royalty-free, -non-exclusive license: - -(a) under intellectual property rights (other than patent or trademark) - Licensable by such Contributor to use, reproduce, make available, - modify, display, perform, distribute, and otherwise exploit its - Contributions, either on an unmodified basis, with Modifications, or - as part of a Larger Work; and - -(b) under Patent Claims of such Contributor to make, use, sell, offer - for sale, have made, import, and otherwise transfer either its - Contributions or its Contributor Version. - -2.2. Effective Date - -The licenses granted in Section 2.1 with respect to any Contribution -become effective for each Contribution on the date the Contributor first -distributes such Contribution. - -2.3. Limitations on Grant Scope - -The licenses granted in this Section 2 are the only rights granted under -this License. No additional rights or licenses will be implied from the -distribution or licensing of Covered Software under this License. -Notwithstanding Section 2.1(b) above, no patent license is granted by a -Contributor: - -(a) for any code that a Contributor has removed from Covered Software; - or - -(b) for infringements caused by: (i) Your and any other third party's - modifications of Covered Software, or (ii) the combination of its - Contributions with other software (except as part of its Contributor - Version); or - -(c) under Patent Claims infringed by Covered Software in the absence of - its Contributions. - -This License does not grant any rights in the trademarks, service marks, -or logos of any Contributor (except as may be necessary to comply with -the notice requirements in Section 3.4). - -2.4. Subsequent Licenses - -No Contributor makes additional grants as a result of Your choice to -distribute the Covered Software under a subsequent version of this -License (see Section 10.2) or under the terms of a Secondary License (if -permitted under the terms of Section 3.3). - -2.5. Representation - -Each Contributor represents that the Contributor believes its -Contributions are its original creation(s) or it has sufficient rights -to grant the rights to its Contributions conveyed by this License. - -2.6. Fair Use - -This License is not intended to limit any rights You have under -applicable copyright doctrines of fair use, fair dealing, or other -equivalents. - -2.7. Conditions - -Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted -in Section 2.1. - -3. Responsibilities -------------------- - -3.1. Distribution of Source Form - -All distribution of Covered Software in Source Code Form, including any -Modifications that You create or to which You contribute, must be under -the terms of this License. You must inform recipients that the Source -Code Form of the Covered Software is governed by the terms of this -License, and how they can obtain a copy of this License. You may not -attempt to alter or restrict the recipients' rights in the Source Code -Form. - -3.2. Distribution of Executable Form - -If You distribute Covered Software in Executable Form then: - -(a) such Covered Software must also be made available in Source Code - Form, as described in Section 3.1, and You must inform recipients of - the Executable Form how they can obtain a copy of such Source Code - Form by reasonable means in a timely manner, at a charge no more - than the cost of distribution to the recipient; and - -(b) You may distribute such Executable Form under the terms of this - License, or sublicense it under different terms, provided that the - license for the Executable Form does not attempt to limit or alter - the recipients' rights in the Source Code Form under this License. - -3.3. Distribution of a Larger Work - -You may create and distribute a Larger Work under terms of Your choice, -provided that You also comply with the requirements of this License for -the Covered Software. If the Larger Work is a combination of Covered -Software with a work governed by one or more Secondary Licenses, and the -Covered Software is not Incompatible With Secondary Licenses, this -License permits You to additionally distribute such Covered Software -under the terms of such Secondary License(s), so that the recipient of -the Larger Work may, at their option, further distribute the Covered -Software under the terms of either this License or such Secondary -License(s). - -3.4. Notices - -You may not remove or alter the substance of any license notices -(including copyright notices, patent notices, disclaimers of warranty, -or limitations of liability) contained within the Source Code Form of -the Covered Software, except that You may alter any license notices to -the extent required to remedy known factual inaccuracies. - -3.5. Application of Additional Terms - -You may choose to offer, and to charge a fee for, warranty, support, -indemnity or liability obligations to one or more recipients of Covered -Software. However, You may do so only on Your own behalf, and not on -behalf of any Contributor. You must make it absolutely clear that any -such warranty, support, indemnity, or liability obligation is offered by -You alone, and You hereby agree to indemnify every Contributor for any -liability incurred by such Contributor as a result of warranty, support, -indemnity or liability terms You offer. You may include additional -disclaimers of warranty and limitations of liability specific to any -jurisdiction. - -4. Inability to Comply Due to Statute or Regulation ---------------------------------------------------- - -If it is impossible for You to comply with any of the terms of this -License with respect to some or all of the Covered Software due to -statute, judicial order, or regulation then You must: (a) comply with -the terms of this License to the maximum extent possible; and (b) -describe the limitations and the code they affect. Such description must -be placed in a text file included with all distributions of the Covered -Software under this License. Except to the extent prohibited by statute -or regulation, such description must be sufficiently detailed for a -recipient of ordinary skill to be able to understand it. - -5. Termination --------------- - -5.1. The rights granted under this License will terminate automatically -if You fail to comply with any of its terms. However, if You become -compliant, then the rights granted under this License from a particular -Contributor are reinstated (a) provisionally, unless and until such -Contributor explicitly and finally terminates Your grants, and (b) on an -ongoing basis, if such Contributor fails to notify You of the -non-compliance by some reasonable means prior to 60 days after You have -come back into compliance. Moreover, Your grants from a particular -Contributor are reinstated on an ongoing basis if such Contributor -notifies You of the non-compliance by some reasonable means, this is the -first time You have received notice of non-compliance with this License -from such Contributor, and You become compliant prior to 30 days after -Your receipt of the notice. - -5.2. If You initiate litigation against any entity by asserting a patent -infringement claim (excluding declaratory judgment actions, -counter-claims, and cross-claims) alleging that a Contributor Version -directly or indirectly infringes any patent, then the rights granted to -You by any and all Contributors for the Covered Software under Section -2.1 of this License shall terminate. - -5.3. In the event of termination under Sections 5.1 or 5.2 above, all -end user license agreements (excluding distributors and resellers) which -have been validly granted by You or Your distributors under this License -prior to termination shall survive termination. - -************************************************************************ -* * -* 6. Disclaimer of Warranty * -* ------------------------- * -* * -* Covered Software is provided under this License on an "as is" * -* basis, without warranty of any kind, either expressed, implied, or * -* statutory, including, without limitation, warranties that the * -* Covered Software is free of defects, merchantable, fit for a * -* particular purpose or non-infringing. The entire risk as to the * -* quality and performance of the Covered Software is with You. * -* Should any Covered Software prove defective in any respect, You * -* (not any Contributor) assume the cost of any necessary servicing, * -* repair, or correction. This disclaimer of warranty constitutes an * -* essential part of this License. No use of any Covered Software is * -* authorized under this License except under this disclaimer. * -* * -************************************************************************ - -************************************************************************ -* * -* 7. Limitation of Liability * -* -------------------------- * -* * -* Under no circumstances and under no legal theory, whether tort * -* (including negligence), contract, or otherwise, shall any * -* Contributor, or anyone who distributes Covered Software as * -* permitted above, be liable to You for any direct, indirect, * -* special, incidental, or consequential damages of any character * -* including, without limitation, damages for lost profits, loss of * -* goodwill, work stoppage, computer failure or malfunction, or any * -* and all other commercial damages or losses, even if such party * -* shall have been informed of the possibility of such damages. This * -* limitation of liability shall not apply to liability for death or * -* personal injury resulting from such party's negligence to the * -* extent applicable law prohibits such limitation. Some * -* jurisdictions do not allow the exclusion or limitation of * -* incidental or consequential damages, so this exclusion and * -* limitation may not apply to You. * -* * -************************************************************************ - -8. Litigation -------------- - -Any litigation relating to this License may be brought only in the -courts of a jurisdiction where the defendant maintains its principal -place of business and such litigation shall be governed by laws of that -jurisdiction, without reference to its conflict-of-law provisions. -Nothing in this Section shall prevent a party's ability to bring -cross-claims or counter-claims. - -9. Miscellaneous ----------------- - -This License represents the complete agreement concerning the subject -matter hereof. If any provision of this License is held to be -unenforceable, such provision shall be reformed only to the extent -necessary to make it enforceable. Any law or regulation which provides -that the language of a contract shall be construed against the drafter -shall not be used to construe this License against a Contributor. - -10. Versions of the License ---------------------------- - -10.1. New Versions - -Mozilla Foundation is the license steward. Except as provided in Section -10.3, no one other than the license steward has the right to modify or -publish new versions of this License. Each version will be given a -distinguishing version number. - -10.2. Effect of New Versions - -You may distribute the Covered Software under the terms of the version -of the License under which You originally received the Covered Software, -or under the terms of any subsequent version published by the license -steward. - -10.3. Modified Versions - -If you create software not governed by this License, and you want to -create a new license for such software, you may create and use a -modified version of this License if you rename the license and remove -any references to the name of the license steward (except to note that -such modified license differs from this License). - -10.4. Distributing Source Code Form that is Incompatible With Secondary -Licenses - -If You choose to distribute Source Code Form that is Incompatible With -Secondary Licenses under the terms of this version of the License, the -notice described in Exhibit B of this License must be attached. - -Exhibit A - Source Code Form License Notice -------------------------------------------- - - This Source Code Form is subject to the terms of the Mozilla Public - License, v. 2.0. If a copy of the MPL was not distributed with this - file, You can obtain one at http://mozilla.org/MPL/2.0/. - -If it is not possible or desirable to put the notice in a particular -file, then You may include the notice in a location (such as a LICENSE -file in a relevant directory) where a recipient would be likely to look -for such a notice. - -You may add additional accurate notices of copyright ownership. - -Exhibit B - "Incompatible With Secondary Licenses" Notice ---------------------------------------------------------- - - This Source Code Form is "Incompatible With Secondary Licenses", as - defined by the Mozilla Public License, v. 2.0. +For questions about this License: +- Repository: https://github.com/hyperpolymath/palimpsest-license +- Council: contact via repository Issues diff --git a/LICENSES/MPL-2.0.txt b/LICENSES/MPL-2.0.txt deleted file mode 100644 index 14e2f77..0000000 --- a/LICENSES/MPL-2.0.txt +++ /dev/null @@ -1,373 +0,0 @@ -Mozilla Public License Version 2.0 -================================== - -1. Definitions --------------- - -1.1. "Contributor" - means each individual or legal entity that creates, contributes to - the creation of, or owns Covered Software. - -1.2. "Contributor Version" - means the combination of the Contributions of others (if any) used - by a Contributor and that particular Contributor's Contribution. - -1.3. "Contribution" - means Covered Software of a particular Contributor. - -1.4. "Covered Software" - means Source Code Form to which the initial Contributor has attached - the notice in Exhibit A, the Executable Form of such Source Code - Form, and Modifications of such Source Code Form, in each case - including portions thereof. - -1.5. "Incompatible With Secondary Licenses" - means - - (a) that the initial Contributor has attached the notice described - in Exhibit B to the Covered Software; or - - (b) that the Covered Software was made available under the terms of - version 1.1 or earlier of the License, but not also under the - terms of a Secondary License. - -1.6. "Executable Form" - means any form of the work other than Source Code Form. - -1.7. "Larger Work" - means a work that combines Covered Software with other material, in - a separate file or files, that is not Covered Software. - -1.8. "License" - means this document. - -1.9. "Licensable" - means having the right to grant, to the maximum extent possible, - whether at the time of the initial grant or subsequently, any and - all of the rights conveyed by this License. - -1.10. "Modifications" - means any of the following: - - (a) any file in Source Code Form that results from an addition to, - deletion from, or modification of the contents of Covered - Software; or - - (b) any new file in Source Code Form that contains any Covered - Software. - -1.11. "Patent Claims" of a Contributor - means any patent claim(s), including without limitation, method, - process, and apparatus claims, in any patent Licensable by such - Contributor that would be infringed, but for the grant of the - License, by the making, using, selling, offering for sale, having - made, import, or transfer of either its Contributions or its - Contributor Version. - -1.12. "Secondary License" - means either the GNU General Public License, Version 2.0, the GNU - Lesser General Public License, Version 2.1, the GNU Affero General - Public License, Version 3.0, or any later versions of those - licenses. - -1.13. "Source Code Form" - means the form of the work preferred for making modifications. - -1.14. "You" (or "Your") - means an individual or a legal entity exercising rights under this - License. For legal entities, "You" includes any entity that - controls, is controlled by, or is under common control with You. For - purposes of this definition, "control" means (a) the power, direct - or indirect, to cause the direction or management of such entity, - whether by contract or otherwise, or (b) ownership of more than - fifty percent (50%) of the outstanding shares or beneficial - ownership of such entity. - -2. License Grants and Conditions --------------------------------- - -2.1. Grants - -Each Contributor hereby grants You a world-wide, royalty-free, -non-exclusive license: - -(a) under intellectual property rights (other than patent or trademark) - Licensable by such Contributor to use, reproduce, make available, - modify, display, perform, distribute, and otherwise exploit its - Contributions, either on an unmodified basis, with Modifications, or - as part of a Larger Work; and - -(b) under Patent Claims of such Contributor to make, use, sell, offer - for sale, have made, import, and otherwise transfer either its - Contributions or its Contributor Version. - -2.2. Effective Date - -The licenses granted in Section 2.1 with respect to any Contribution -become effective for each Contribution on the date the Contributor first -distributes such Contribution. - -2.3. Limitations on Grant Scope - -The licenses granted in this Section 2 are the only rights granted under -this License. No additional rights or licenses will be implied from the -distribution or licensing of Covered Software under this License. -Notwithstanding Section 2.1(b) above, no patent license is granted by a -Contributor: - -(a) for any code that a Contributor has removed from Covered Software; - or - -(b) for infringements caused by: (i) Your and any other third party's - modifications of Covered Software, or (ii) the combination of its - Contributions with other software (except as part of its Contributor - Version); or - -(c) under Patent Claims infringed by Covered Software in the absence of - its Contributions. - -This License does not grant any rights in the trademarks, service marks, -or logos of any Contributor (except as may be necessary to comply with -the notice requirements in Section 3.4). - -2.4. Subsequent Licenses - -No Contributor makes additional grants as a result of Your choice to -distribute the Covered Software under a subsequent version of this -License (see Section 10.2) or under the terms of a Secondary License (if -permitted under the terms of Section 3.3). - -2.5. Representation - -Each Contributor represents that the Contributor believes its -Contributions are its original creation(s) or it has sufficient rights -to grant the rights to its Contributions conveyed by this License. - -2.6. Fair Use - -This License is not intended to limit any rights You have under -applicable copyright doctrines of fair use, fair dealing, or other -equivalents. - -2.7. Conditions - -Sections 3.1, 3.2, 3.3, and 3.4 are conditions of the licenses granted -in Section 2.1. - -3. Responsibilities -------------------- - -3.1. Distribution of Source Form - -All distribution of Covered Software in Source Code Form, including any -Modifications that You create or to which You contribute, must be under -the terms of this License. You must inform recipients that the Source -Code Form of the Covered Software is governed by the terms of this -License, and how they can obtain a copy of this License. You may not -attempt to alter or restrict the recipients' rights in the Source Code -Form. - -3.2. Distribution of Executable Form - -If You distribute Covered Software in Executable Form then: - -(a) such Covered Software must also be made available in Source Code - Form, as described in Section 3.1, and You must inform recipients of - the Executable Form how they can obtain a copy of such Source Code - Form by reasonable means in a timely manner, at a charge no more - than the cost of distribution to the recipient; and - -(b) You may distribute such Executable Form under the terms of this - License, or sublicense it under different terms, provided that the - license for the Executable Form does not attempt to limit or alter - the recipients' rights in the Source Code Form under this License. - -3.3. Distribution of a Larger Work - -You may create and distribute a Larger Work under terms of Your choice, -provided that You also comply with the requirements of this License for -the Covered Software. If the Larger Work is a combination of Covered -Software with a work governed by one or more Secondary Licenses, and the -Covered Software is not Incompatible With Secondary Licenses, this -License permits You to additionally distribute such Covered Software -under the terms of such Secondary License(s), so that the recipient of -the Larger Work may, at their option, further distribute the Covered -Software under the terms of either this License or such Secondary -License(s). - -3.4. Notices - -You may not remove or alter the substance of any license notices -(including copyright notices, patent notices, disclaimers of warranty, -or limitations of liability) contained within the Source Code Form of -the Covered Software, except that You may alter any license notices to -the extent required to remedy known factual inaccuracies. - -3.5. Application of Additional Terms - -You may choose to offer, and to charge a fee for, warranty, support, -indemnity or liability obligations to one or more recipients of Covered -Software. However, You may do so only on Your own behalf, and not on -behalf of any Contributor. You must make it absolutely clear that any -such warranty, support, indemnity, or liability obligation is offered by -You alone, and You hereby agree to indemnify every Contributor for any -liability incurred by such Contributor as a result of warranty, support, -indemnity or liability terms You offer. You may include additional -disclaimers of warranty and limitations of liability specific to any -jurisdiction. - -4. Inability to Comply Due to Statute or Regulation ---------------------------------------------------- - -If it is impossible for You to comply with any of the terms of this -License with respect to some or all of the Covered Software due to -statute, judicial order, or regulation then You must: (a) comply with -the terms of this License to the maximum extent possible; and (b) -describe the limitations and the code they affect. Such description must -be placed in a text file included with all distributions of the Covered -Software under this License. Except to the extent prohibited by statute -or regulation, such description must be sufficiently detailed for a -recipient of ordinary skill to be able to understand it. - -5. Termination --------------- - -5.1. The rights granted under this License will terminate automatically -if You fail to comply with any of its terms. However, if You become -compliant, then the rights granted under this License from a particular -Contributor are reinstated (a) provisionally, unless and until such -Contributor explicitly and finally terminates Your grants, and (b) on an -ongoing basis, if such Contributor fails to notify You of the -non-compliance by some reasonable means prior to 60 days after You have -come back into compliance. Moreover, Your grants from a particular -Contributor are reinstated on an ongoing basis if such Contributor -notifies You of the non-compliance by some reasonable means, this is the -first time You have received notice of non-compliance with this License -from such Contributor, and You become compliant prior to 30 days after -Your receipt of the notice. - -5.2. If You initiate litigation against any entity by asserting a patent -infringement claim (excluding declaratory judgment actions, -counter-claims, and cross-claims) alleging that a Contributor Version -directly or indirectly infringes any patent, then the rights granted to -You by any and all Contributors for the Covered Software under Section -2.1 of this License shall terminate. - -5.3. In the event of termination under Sections 5.1 or 5.2 above, all -end user license agreements (excluding distributors and resellers) which -have been validly granted by You or Your distributors under this License -prior to termination shall survive termination. - -************************************************************************ -* * -* 6. Disclaimer of Warranty * -* ------------------------- * -* * -* Covered Software is provided under this License on an "as is" * -* basis, without warranty of any kind, either expressed, implied, or * -* statutory, including, without limitation, warranties that the * -* Covered Software is free of defects, merchantable, fit for a * -* particular purpose or non-infringing. The entire risk as to the * -* quality and performance of the Covered Software is with You. * -* Should any Covered Software prove defective in any respect, You * -* (not any Contributor) assume the cost of any necessary servicing, * -* repair, or correction. This disclaimer of warranty constitutes an * -* essential part of this License. No use of any Covered Software is * -* authorized under this License except under this disclaimer. * -* * -************************************************************************ - -************************************************************************ -* * -* 7. Limitation of Liability * -* -------------------------- * -* * -* Under no circumstances and under no legal theory, whether tort * -* (including negligence), contract, or otherwise, shall any * -* Contributor, or anyone who distributes Covered Software as * -* permitted above, be liable to You for any direct, indirect, * -* special, incidental, or consequential damages of any character * -* including, without limitation, damages for lost profits, loss of * -* goodwill, work stoppage, computer failure or malfunction, or any * -* and all other commercial damages or losses, even if such party * -* shall have been informed of the possibility of such damages. This * -* limitation of liability shall not apply to liability for death or * -* personal injury resulting from such party's negligence to the * -* extent applicable law prohibits such limitation. Some * -* jurisdictions do not allow the exclusion or limitation of * -* incidental or consequential damages, so this exclusion and * -* limitation may not apply to You. * -* * -************************************************************************ - -8. Litigation -------------- - -Any litigation relating to this License may be brought only in the -courts of a jurisdiction where the defendant maintains its principal -place of business and such litigation shall be governed by laws of that -jurisdiction, without reference to its conflict-of-law provisions. -Nothing in this Section shall prevent a party's ability to bring -cross-claims or counter-claims. - -9. Miscellaneous ----------------- - -This License represents the complete agreement concerning the subject -matter hereof. If any provision of this License is held to be -unenforceable, such provision shall be reformed only to the extent -necessary to make it enforceable. Any law or regulation which provides -that the language of a contract shall be construed against the drafter -shall not be used to construe this License against a Contributor. - -10. Versions of the License ---------------------------- - -10.1. New Versions - -Mozilla Foundation is the license steward. Except as provided in Section -10.3, no one other than the license steward has the right to modify or -publish new versions of this License. Each version will be given a -distinguishing version number. - -10.2. Effect of New Versions - -You may distribute the Covered Software under the terms of the version -of the License under which You originally received the Covered Software, -or under the terms of any subsequent version published by the license -steward. - -10.3. Modified Versions - -If you create software not governed by this License, and you want to -create a new license for such software, you may create and use a -modified version of this License if you rename the license and remove -any references to the name of the license steward (except to note that -such modified license differs from this License). - -10.4. Distributing Source Code Form that is Incompatible With Secondary -Licenses - -If You choose to distribute Source Code Form that is Incompatible With -Secondary Licenses under the terms of this version of the License, the -notice described in Exhibit B of this License must be attached. - -Exhibit A - Source Code Form License Notice -------------------------------------------- - - This Source Code Form is subject to the terms of the Mozilla Public - License, v. 2.0. If a copy of the MPL was not distributed with this - file, You can obtain one at http://mozilla.org/MPL/2.0/. - -If it is not possible or desirable to put the notice in a particular -file, then You may include the notice in a location (such as a LICENSE -file in a relevant directory) where a recipient would be likely to look -for such a notice. - -You may add additional accurate notices of copyright ownership. - -Exhibit B - "Incompatible With Secondary Licenses" Notice ---------------------------------------------------------- - - This Source Code Form is "Incompatible With Secondary Licenses", as - defined by the Mozilla Public License, v. 2.0. diff --git a/NOTICE b/NOTICE index ae0bc80..9f88f33 100644 --- a/NOTICE +++ b/NOTICE @@ -4,19 +4,10 @@ Licensing Notice This project is authored by Jonathan D.A. Jewell (hyperpolymath) and is licensed under the Palimpsest License (PMPL-1.0-or-later). -The PMPL-1.0-or-later is a philosophical extension of the Mozilla Public -License 2.0, adding provisions for cryptographic provenance, emotional -lineage preservation, and quantum-safe signatures. The full PMPL text is -available in LICENSES/PMPL-1.0-or-later.txt. +The full license text is in LICENSE and LICENSES/PMPL-1.0-or-later.txt. +All source files carry the SPDX identifier: -For compatibility with automated license detection tools and platforms -that require OSI-approved licenses, the root LICENSE file contains the -standard Mozilla Public License 2.0 text. This ensures that package -registries, CI systems, and other tooling correctly identify the license. - -The legally binding terms are: - - Source files: governed by PMPL-1.0-or-later (per SPDX headers) - - Combined works: compatible with MPL-2.0 (per PMPL Section 6) + SPDX-License-Identifier: PMPL-1.0-or-later For more information about the Palimpsest License: https://github.com/hyperpolymath/palimpsest-license diff --git a/README.adoc b/README.adoc index 9ca1b58..469c38f 100644 --- a/README.adoc +++ b/README.adoc @@ -16,119 +16,9 @@ image:https://img.shields.io/badge/RSR-Bronze-cd7f32[RSR Compliance] ==== **AI-Assisted Install:** Just tell any AI: + `Set up NeuroPhone on my Android from https://github.com/hyperpolymath/neurophone` + -It reads this repo, asks a few questions, and does everything. <>. +It reads this repo, asks a few questions, and does everything. See link:docs/installation.adoc[Installation]. ==== -[[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 the <> section below. - -''' - == What This Is **neurophone** is a complete *Android application* for neurosymbolic AI on mobile devices. It combines spiking neural networks with large language models for on-device intelligence. @@ -204,242 +94,24 @@ Also compatible with Android 8.0+ devices with 4GB+ RAM. | Often sent to cloud |=== -== 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) +== Installation -Reservoir for state prediction: +The fastest way: tell any AI assistant to set it up for you. See link:docs/AI_INSTALLATION_GUIDE.adoc[AI Installation Guide] for the full recipe, and link:docs/installation.adoc[Installation] for the step-by-step walkthrough (privacy notice, troubleshooting, uninstall). -* 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 - -[[getting-started]] -== 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 -``` - -== 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; -``` - -== 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 +[source,text] +---- +Set up NeuroPhone on my Android from https://github.com/hyperpolymath/neurophone +---- -| Bridge integration -| <1ms -| Per step +For manual installation, see link:docs/build.adoc[Building NeuroPhone]. -| Local LLM (1B) -| 50-100ms/token -| Q4 quantized +== Documentation -| Claude API -| 500-2000ms -| Network dependent -|=== +* link:docs/architecture.adoc[Architecture] -- Rust crates, Android app, components, performance, topology +* link:docs/usage.adoc[Usage] -- Kotlin and Rust APIs +* link:docs/build.adoc[Building NeuroPhone] -- prerequisites, build, model download, configuration, development +* link:docs/installation.adoc[Installation] -- AI-assisted install, privacy, troubleshooting +* link:docs/AI_INSTALLATION_GUIDE.adoc[AI Installation Guide] -- machine-readable install recipe == Relationship to mobile-ai-orchestrator @@ -502,19 +174,6 @@ Bronze-level RSR (Rhodium Standard Repository) compliance: * Build automation * Security policy -== Development - -```bash -# Run tests -cargo test - -# Build for Android -./scripts/build-android.sh - -# Generate docs -cargo doc --open -``` - == Contributing Contributions welcome! See link:CONTRIBUTING.md[CONTRIBUTING.md]. @@ -543,8 +202,3 @@ Palimpsest-MPL-1.0 License - See LICENSE file --- *Android Application • On-Device Neural Processing • Spiking Networks • Local LLM* - - -== Architecture - -See link:TOPOLOGY.md[TOPOLOGY.md] for a visual architecture map and completion dashboard. diff --git a/android/app/src/main/java/ai/neurophone/MainActivity.kt b/android/app/src/main/java/ai/neurophone/MainActivity.kt index 0c07302..6df619e 100644 --- a/android/app/src/main/java/ai/neurophone/MainActivity.kt +++ b/android/app/src/main/java/ai/neurophone/MainActivity.kt @@ -1,3 +1,5 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell package ai.neurophone import android.Manifest diff --git a/android/app/src/main/java/ai/neurophone/NativeLib.kt b/android/app/src/main/java/ai/neurophone/NativeLib.kt index 454b605..9799c45 100644 --- a/android/app/src/main/java/ai/neurophone/NativeLib.kt +++ b/android/app/src/main/java/ai/neurophone/NativeLib.kt @@ -1,3 +1,5 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell package ai.neurophone /** diff --git a/crates/claude-client/src/lib.rs b/crates/claude-client/src/lib.rs index f289adc..a7cb36b 100644 --- a/crates/claude-client/src/lib.rs +++ b/crates/claude-client/src/lib.rs @@ -1,3 +1,7 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// NeuroPhone - High-Assurance Hardware Orchestration +// Copyright (c) 2026 Jonathan D.A. Jewell + //! Claude API Client - Cloud Connection //! //! Connects to Claude (Anthropic's AI) for advanced reasoning diff --git a/crates/esn/src/lib.rs b/crates/esn/src/lib.rs index 9d004cc..e514cf9 100644 --- a/crates/esn/src/lib.rs +++ b/crates/esn/src/lib.rs @@ -9,7 +9,7 @@ //! The ESN serves as a secondary reservoir in the neurosymbolic pipeline, //! operating on transformed LSM outputs for higher-level temporal features. -#![allow(unsafe_code)] +#![deny(unsafe_code)] use ndarray::{Array1, Array2}; use ndarray_rand::rand_distr::{Normal, Uniform}; diff --git a/crates/lsm/src/lib.rs b/crates/lsm/src/lib.rs index e65404e..2f836a5 100644 --- a/crates/lsm/src/lib.rs +++ b/crates/lsm/src/lib.rs @@ -1,3 +1,7 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later +// NeuroPhone - High-Assurance Hardware Orchestration +// Copyright (c) 2026 Jonathan D.A. Jewell + //! Liquid State Machine (LSM) - Spiking Neural Network Reservoir //! //! Implements a biologically-inspired spiking neural network using @@ -5,7 +9,7 @@ //! This serves as the first reservoir in our neurosymbolic pipeline, //! processing temporal sensor data with spike-timing dynamics. -#![allow(unsafe_code)] +#![deny(unsafe_code)] use ndarray::{Array1, Array2, Axis}; use ndarray_rand::rand_distr::{Bernoulli, Normal, Uniform}; use ndarray_rand::RandomExt; diff --git a/docs/architecture.adoc b/docs/architecture.adoc new file mode 100644 index 0000000..9af82ff --- /dev/null +++ b/docs/architecture.adoc @@ -0,0 +1,149 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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..d7021ab --- /dev/null +++ b/docs/build.adoc @@ -0,0 +1,72 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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/governance/CRG-AUDIT-2026-04-18.adoc b/docs/governance/CRG-AUDIT-2026-04-18.adoc index 3cd59b4..b93890f 100644 --- a/docs/governance/CRG-AUDIT-2026-04-18.adoc +++ b/docs/governance/CRG-AUDIT-2026-04-18.adoc @@ -77,7 +77,7 @@ Publication requires B+. Long alpha is discipline, not shame. | Very thin relative to gossamer/boj-server annotation bars | `LICENSE` + `LICENSES/` directory -| PRESENT (`LICENSE`, `LICENSES/PMPL-1.0-or-later.txt`, `LICENSES/MPL-2.0.txt`) +| PRESENT (`LICENSE`, `LICENSES/PMPL-1.0-or-later.txt`) | Good licence hygiene structurally, but *see merge conflicts below* | `guix.scm` + `flake.nix` @@ -144,7 +144,7 @@ Sample (`.github/workflows/rust-ci.yml` lines 1-5): <<<<<<< HEAD # SPDX-License-Identifier: PMPL-1.0-or-later ======= -# SPDX-License-Identifier: MPL-2.0-or-later +# SPDX-License-Identifier: >>>>>>> 0a372d5 (chore: sync from parent repo automation) name: Rust CI ---- @@ -385,7 +385,7 @@ What blocks *immediate* promotion to D (do these first): hand-merge of each file, delete all `<<<<<<< HEAD` / `=======` / `>>>>>>> ` marker lines. Verify with `rg '^<<<<<<< HEAD|^>>>>>>> '` returns zero. Keep the - PMPL-1.0-or-later SPDX line (drop the `MPL-2.0-or-later` variant per + PMPL-1.0-or-later SPDX line (drop the non-canonical variant per Rule 1 of the licence policy). . **Make `rust-ci.yml` actually run.** Once conflicts are resolved, trigger a CI run and record the green SHA in STATE.a2ml. diff --git a/docs/installation.adoc b/docs/installation.adoc new file mode 100644 index 0000000..0a6cd09 --- /dev/null +++ b/docs/installation.adoc @@ -0,0 +1,113 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md index 3517441..82ae5e9 100644 --- a/docs/tech-debt-2026-05-26.md +++ b/docs/tech-debt-2026-05-26.md @@ -1,5 +1,5 @@ @@ -22,9 +22,9 @@ No proof-bearing files (`*.v`, `*.lean`, `*.agda`, `*.idr`, `*.idr2`, `*.fst`, ` | Field | Value | |---|---| | LICENSE file | `LICENSE` | -| SPDX header | `MPL-2.0` | -| Manifest licence | `MPL-2.0` | -| Body classifier | `Palimp-MPL-2.0` | +| SPDX header | `PMPL-1.0-or-later` | +| Manifest licence | `PMPL-1.0-or-later` | +| Body classifier | `PMPL-1.0-or-later` | | Severity | `ok` | **Recommended next move:** none for licence. diff --git a/docs/usage.adoc b/docs/usage.adoc new file mode 100644 index 0000000..3fcc50f --- /dev/null +++ b/docs/usage.adoc @@ -0,0 +1,41 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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..2a7d9c2 --- /dev/null +++ b/proofs/README.adoc @@ -0,0 +1,56 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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..1c6d172 --- /dev/null +++ b/proofs/dafny/README.adoc @@ -0,0 +1,14 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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..794c89a --- /dev/null +++ b/proofs/lean/README.adoc @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: PMPL-1.0-or-later += 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..0b7fe63 --- /dev/null +++ b/proofs/tla/Lifecycle.tla @@ -0,0 +1,55 @@ +---------------------------- MODULE Lifecycle ---------------------------- +(* SPDX-License-Identifier: PMPL-1.0-or-later *) +(* 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) +==========================================================================