diff --git a/.devcontainer/README.adoc b/.devcontainer/README.adoc index 155105d..ba51fcd 100644 --- a/.devcontainer/README.adoc +++ b/.devcontainer/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Dev Container Usage :author: Jonathan D.A. Jewell diff --git a/.github/GOVERNANCE.md b/.github/GOVERNANCE.md index 1e27676..dd3a40c 100644 --- a/.github/GOVERNANCE.md +++ b/.github/GOVERNANCE.md @@ -1,4 +1,4 @@ - + # Project Governance diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md index 85f3113..6e2bea9 100644 --- a/.github/copilot-instructions.md +++ b/.github/copilot-instructions.md @@ -1,4 +1,4 @@ - + diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md index 63eb6ad..3a8accd 100644 --- a/.github/pull_request_template.md +++ b/.github/pull_request_template.md @@ -1,4 +1,4 @@ - + ## Summary diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 3236941..e3c0a50 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 name: Governance on: diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 9825379..45980c9 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 name: Hypatia Security Scan on: diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 176388a..a8bf0cb 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,4 +1,4 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 name: OSSF Scorecard on: diff --git a/.machine_readable/bot_directives/README.adoc b/.machine_readable/bot_directives/README.adoc index bdb5d56..03e6a7c 100644 --- a/.machine_readable/bot_directives/README.adoc +++ b/.machine_readable/bot_directives/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = Bot Directives :toc: preamble diff --git a/.machine_readable/svc/k9/README.adoc b/.machine_readable/svc/k9/README.adoc index 143e746..005ce58 100644 --- a/.machine_readable/svc/k9/README.adoc +++ b/.machine_readable/svc/k9/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = K9 Contractiles :toc: left :icons: font diff --git a/CODE_OF_CONDUCT.md b/CODE_OF_CONDUCT.md index 1f1548c..caeda1c 100644 --- a/CODE_OF_CONDUCT.md +++ b/CODE_OF_CONDUCT.md @@ -1,4 +1,4 @@ - + # Contributor Covenant Code of Conduct ## Our Pledge diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index a7e0669..80ecdac 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -1,4 +1,4 @@ - + # Contributing Thank you for your interest in contributing! We follow a "Dual-Track" architecture where human-readable documentation lives in the root and machine-readable policies live in `.machine_readable/`. diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index c661636..6062cfa 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell = Gossamer — Show Me The Receipts :toc: diff --git a/LICENSE b/LICENSE index 2a8b960..14e2f77 100644 --- a/LICENSE +++ b/LICENSE @@ -1,5 +1,3 @@ -SPDX-License-Identifier: MPL-2.0 - Mozilla Public License Version 2.0 ================================== diff --git a/LICENSES/CC-BY-SA-4.0.txt b/LICENSES/CC-BY-SA-4.0.txt new file mode 100644 index 0000000..835a683 --- /dev/null +++ b/LICENSES/CC-BY-SA-4.0.txt @@ -0,0 +1,170 @@ +Creative Commons Attribution-ShareAlike 4.0 International + + Creative Commons Corporation (“Creative Commons”) is not a law firm and does not provide legal services or legal advice. Distribution of Creative Commons public licenses does not create a lawyer-client or other relationship. Creative Commons makes its licenses and related information available on an “as-is” basis. Creative Commons gives no warranties regarding its licenses, any material licensed under their terms and conditions, or any related information. Creative Commons disclaims all liability for damages resulting from their use to the fullest extent possible. + +Using Creative Commons Public Licenses + +Creative Commons public licenses provide a standard set of terms and conditions that creators and other rights holders may use to share original works of authorship and other material subject to copyright and certain other rights specified in the public license below. The following considerations are for informational purposes only, are not exhaustive, and do not form part of our licenses. + +Considerations for licensors: Our public licenses are intended for use by those authorized to give the public permission to use material in ways otherwise restricted by copyright and certain other rights. Our licenses are irrevocable. Licensors should read and understand the terms and conditions of the license they choose before applying it. Licensors should also secure all rights necessary before applying our licenses so that the public can reuse the material as expected. Licensors should clearly mark any material not subject to the license. This includes other CC-licensed material, or material used under an exception or limitation to copyright. More considerations for licensors. + +Considerations for the public: By using one of our public licenses, a licensor grants the public permission to use the licensed material under specified terms and conditions. If the licensor’s permission is not necessary for any reason–for example, because of any applicable exception or limitation to copyright–then that use is not regulated by the license. Our licenses grant only permissions under copyright and certain other rights that a licensor has authority to grant. Use of the licensed material may still be restricted for other reasons, including because others have copyright or other rights in the material. A licensor may make special requests, such as asking that all changes be marked or described. + +Although not required by our licenses, you are encouraged to respect those requests where reasonable. More considerations for the public. + +Creative Commons Attribution-ShareAlike 4.0 International Public License + +By exercising the Licensed Rights (defined below), You accept and agree to be bound by the terms and conditions of this Creative Commons Attribution-ShareAlike 4.0 International Public License ("Public License"). To the extent this Public License may be interpreted as a contract, You are granted the Licensed Rights in consideration of Your acceptance of these terms and conditions, and the Licensor grants You such rights in consideration of benefits the Licensor receives from making the Licensed Material available under these terms and conditions. + +Section 1 – Definitions. + + a. Adapted Material means material subject to Copyright and Similar Rights that is derived from or based upon the Licensed Material and in which the Licensed Material is translated, altered, arranged, transformed, or otherwise modified in a manner requiring permission under the Copyright and Similar Rights held by the Licensor. For purposes of this Public License, where the Licensed Material is a musical work, performance, or sound recording, Adapted Material is always produced where the Licensed Material is synched in timed relation with a moving image. + + b. Adapter's License means the license You apply to Your Copyright and Similar Rights in Your contributions to Adapted Material in accordance with the terms and conditions of this Public License. + + c. BY-SA Compatible License means a license listed at creativecommons.org/compatiblelicenses, approved by Creative Commons as essentially the equivalent of this Public License. + + d. Copyright and Similar Rights means copyright and/or similar rights closely related to copyright including, without limitation, performance, broadcast, sound recording, and Sui Generis Database Rights, without regard to how the rights are labeled or categorized. For purposes of this Public License, the rights specified in Section 2(b)(1)-(2) are not Copyright and Similar Rights. + + e. Effective Technological Measures means those measures that, in the absence of proper authority, may not be circumvented under laws fulfilling obligations under Article 11 of the WIPO Copyright Treaty adopted on December 20, 1996, and/or similar international agreements. + + f. Exceptions and Limitations means fair use, fair dealing, and/or any other exception or limitation to Copyright and Similar Rights that applies to Your use of the Licensed Material. + + g. License Elements means the license attributes listed in the name of a Creative Commons Public License. The License Elements of this Public License are Attribution and ShareAlike. + + h. Licensed Material means the artistic or literary work, database, or other material to which the Licensor applied this Public License. + + i. Licensed Rights means the rights granted to You subject to the terms and conditions of this Public License, which are limited to all Copyright and Similar Rights that apply to Your use of the Licensed Material and that the Licensor has authority to license. + + j. Licensor means the individual(s) or entity(ies) granting rights under this Public License. + + k. Share means to provide material to the public by any means or process that requires permission under the Licensed Rights, such as reproduction, public display, public performance, distribution, dissemination, communication, or importation, and to make material available to the public including in ways that members of the public may access the material from a place and at a time individually chosen by them. + + l. Sui Generis Database Rights means rights other than copyright resulting from Directive 96/9/EC of the European Parliament and of the Council of 11 March 1996 on the legal protection of databases, as amended and/or succeeded, as well as other essentially equivalent rights anywhere in the world. + + m. You means the individual or entity exercising the Licensed Rights under this Public License. Your has a corresponding meaning. + +Section 2 – Scope. + + a. License grant. + + 1. Subject to the terms and conditions of this Public License, the Licensor hereby grants You a worldwide, royalty-free, non-sublicensable, non-exclusive, irrevocable license to exercise the Licensed Rights in the Licensed Material to: + + A. reproduce and Share the Licensed Material, in whole or in part; and + + B. produce, reproduce, and Share Adapted Material. + + 2. Exceptions and Limitations. For the avoidance of doubt, where Exceptions and Limitations apply to Your use, this Public License does not apply, and You do not need to comply with its terms and conditions. + + 3. Term. The term of this Public License is specified in Section 6(a). + + 4. Media and formats; technical modifications allowed. The Licensor authorizes You to exercise the Licensed Rights in all media and formats whether now known or hereafter created, and to make technical modifications necessary to do so. The Licensor waives and/or agrees not to assert any right or authority to forbid You from making technical modifications necessary to exercise the Licensed Rights, including technical modifications necessary to circumvent Effective Technological Measures. For purposes of this Public License, simply making modifications authorized by this Section 2(a)(4) never produces Adapted Material. + + 5. Downstream recipients. + + A. Offer from the Licensor – Licensed Material. Every recipient of the Licensed Material automatically receives an offer from the Licensor to exercise the Licensed Rights under the terms and conditions of this Public License. + + B. Additional offer from the Licensor – Adapted Material. Every recipient of Adapted Material from You automatically receives an offer from the Licensor to exercise the Licensed Rights in the Adapted Material under the conditions of the Adapter’s License You apply. + + C. No downstream restrictions. You may not offer or impose any additional or different terms or conditions on, or apply any Effective Technological Measures to, the Licensed Material if doing so restricts exercise of the Licensed Rights by any recipient of the Licensed Material. + + 6. No endorsement. Nothing in this Public License constitutes or may be construed as permission to assert or imply that You are, or that Your use of the Licensed Material is, connected with, or sponsored, endorsed, or granted official status by, the Licensor or others designated to receive attribution as provided in Section 3(a)(1)(A)(i). + + b. Other rights. + + 1. Moral rights, such as the right of integrity, are not licensed under this Public License, nor are publicity, privacy, and/or other similar personality rights; however, to the extent possible, the Licensor waives and/or agrees not to assert any such rights held by the Licensor to the limited extent necessary to allow You to exercise the Licensed Rights, but not otherwise. + + 2. Patent and trademark rights are not licensed under this Public License. + + 3. To the extent possible, the Licensor waives any right to collect royalties from You for the exercise of the Licensed Rights, whether directly or through a collecting society under any voluntary or waivable statutory or compulsory licensing scheme. In all other cases the Licensor expressly reserves any right to collect such royalties. + +Section 3 – License Conditions. + +Your exercise of the Licensed Rights is expressly made subject to the following conditions. + + a. Attribution. + + 1. If You Share the Licensed Material (including in modified form), You must: + + A. retain the following if it is supplied by the Licensor with the Licensed Material: + + i. identification of the creator(s) of the Licensed Material and any others designated to receive attribution, in any reasonable manner requested by the Licensor (including by pseudonym if designated); + + ii. a copyright notice; + + iii. a notice that refers to this Public License; + + iv. a notice that refers to the disclaimer of warranties; + + v. a URI or hyperlink to the Licensed Material to the extent reasonably practicable; + + B. indicate if You modified the Licensed Material and retain an indication of any previous modifications; and + + C. indicate the Licensed Material is licensed under this Public License, and include the text of, or the URI or hyperlink to, this Public License. + + 2. You may satisfy the conditions in Section 3(a)(1) in any reasonable manner based on the medium, means, and context in which You Share the Licensed Material. For example, it may be reasonable to satisfy the conditions by providing a URI or hyperlink to a resource that includes the required information. + + 3. If requested by the Licensor, You must remove any of the information required by Section 3(a)(1)(A) to the extent reasonably practicable. + + b. ShareAlike.In addition to the conditions in Section 3(a), if You Share Adapted Material You produce, the following conditions also apply. + + 1. The Adapter’s License You apply must be a Creative Commons license with the same License Elements, this version or later, or a BY-SA Compatible License. + + 2. You must include the text of, or the URI or hyperlink to, the Adapter's License You apply. You may satisfy this condition in any reasonable manner based on the medium, means, and context in which You Share Adapted Material. + + 3. You may not offer or impose any additional or different terms or conditions on, or apply any Effective Technological Measures to, Adapted Material that restrict exercise of the rights granted under the Adapter's License You apply. + +Section 4 – Sui Generis Database Rights. + +Where the Licensed Rights include Sui Generis Database Rights that apply to Your use of the Licensed Material: + + a. for the avoidance of doubt, Section 2(a)(1) grants You the right to extract, reuse, reproduce, and Share all or a substantial portion of the contents of the database; + + b. if You include all or a substantial portion of the database contents in a database in which You have Sui Generis Database Rights, then the database in which You have Sui Generis Database Rights (but not its individual contents) is Adapted Material, including for purposes of Section 3(b); and + + c. You must comply with the conditions in Section 3(a) if You Share all or a substantial portion of the contents of the database. +For the avoidance of doubt, this Section 4 supplements and does not replace Your obligations under this Public License where the Licensed Rights include other Copyright and Similar Rights. + +Section 5 – Disclaimer of Warranties and Limitation of Liability. + + a. Unless otherwise separately undertaken by the Licensor, to the extent possible, the Licensor offers the Licensed Material as-is and as-available, and makes no representations or warranties of any kind concerning the Licensed Material, whether express, implied, statutory, or other. This includes, without limitation, warranties of title, merchantability, fitness for a particular purpose, non-infringement, absence of latent or other defects, accuracy, or the presence or absence of errors, whether or not known or discoverable. Where disclaimers of warranties are not allowed in full or in part, this disclaimer may not apply to You. + + b. To the extent possible, in no event will the Licensor be liable to You on any legal theory (including, without limitation, negligence) or otherwise for any direct, special, indirect, incidental, consequential, punitive, exemplary, or other losses, costs, expenses, or damages arising out of this Public License or use of the Licensed Material, even if the Licensor has been advised of the possibility of such losses, costs, expenses, or damages. Where a limitation of liability is not allowed in full or in part, this limitation may not apply to You. + + c. The disclaimer of warranties and limitation of liability provided above shall be interpreted in a manner that, to the extent possible, most closely approximates an absolute disclaimer and waiver of all liability. + +Section 6 – Term and Termination. + + a. This Public License applies for the term of the Copyright and Similar Rights licensed here. However, if You fail to comply with this Public License, then Your rights under this Public License terminate automatically. + + b. Where Your right to use the Licensed Material has terminated under Section 6(a), it reinstates: + + 1. automatically as of the date the violation is cured, provided it is cured within 30 days of Your discovery of the violation; or + + 2. upon express reinstatement by the Licensor. + + c. For the avoidance of doubt, this Section 6(b) does not affect any right the Licensor may have to seek remedies for Your violations of this Public License. + + d. For the avoidance of doubt, the Licensor may also offer the Licensed Material under separate terms or conditions or stop distributing the Licensed Material at any time; however, doing so will not terminate this Public License. + + e. Sections 1, 5, 6, 7, and 8 survive termination of this Public License. + +Section 7 – Other Terms and Conditions. + + a. The Licensor shall not be bound by any additional or different terms or conditions communicated by You unless expressly agreed. + + b. Any arrangements, understandings, or agreements regarding the Licensed Material not stated herein are separate from and independent of the terms and conditions of this Public License. + +Section 8 – Interpretation. + + a. For the avoidance of doubt, this Public License does not, and shall not be interpreted to, reduce, limit, restrict, or impose conditions on any use of the Licensed Material that could lawfully be made without permission under this Public License. + + b. To the extent possible, if any provision of this Public License is deemed unenforceable, it shall be automatically reformed to the minimum extent necessary to make it enforceable. If the provision cannot be reformed, it shall be severed from this Public License without affecting the enforceability of the remaining terms and conditions. + + c. No term or condition of this Public License will be waived and no failure to comply consented to unless expressly agreed to by the Licensor. + + d. Nothing in this Public License constitutes or may be interpreted as a limitation upon, or waiver of, any privileges and immunities that apply to the Licensor or You, including from the legal processes of any jurisdiction or authority. + +Creative Commons is not a party to its public licenses. Notwithstanding, Creative Commons may elect to apply one of its public licenses to material it publishes and in those instances will be considered the “Licensor.” Except for the limited purpose of indicating that material is shared under a Creative Commons public license or as otherwise permitted by the Creative Commons policies published at creativecommons.org/policies, Creative Commons does not authorize the use of the trademark “Creative Commons” or any other trademark or logo of Creative Commons without its prior written consent including, without limitation, in connection with any unauthorized modifications to any of its public licenses or any other arrangements, understandings, or agreements concerning use of licensed material. For the avoidance of doubt, this paragraph does not form part of the public licenses. + +Creative Commons may be contacted at creativecommons.org. diff --git a/LICENSES/MPL-2.0.txt b/LICENSES/MPL-2.0.txt new file mode 100644 index 0000000..14e2f77 --- /dev/null +++ b/LICENSES/MPL-2.0.txt @@ -0,0 +1,373 @@ +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/NEXT-STEPS.md b/NEXT-STEPS.md index e8d5e6a..da2853f 100644 --- a/NEXT-STEPS.md +++ b/NEXT-STEPS.md @@ -1,6 +1,6 @@ # Gossamer — Next Steps - + ## Completed (2026-03-21/22) diff --git a/QUICKSTART-USER.adoc b/QUICKSTART-USER.adoc index bbeb32e..d1ff39d 100644 --- a/QUICKSTART-USER.adoc +++ b/QUICKSTART-USER.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) // // QUICKSTART-USER.adoc — Get Gossamer running from zero diff --git a/README.adoc b/README.adoc index 85f77a5..71f11f9 100644 --- a/README.adoc +++ b/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // SPDX-FileCopyrightText: 2025-2026 Jonathan D.A. Jewell = Gossamer @@ -6,7 +6,7 @@ :toclevels: 2 image:https://img.shields.io/badge/OpenSSF-Best_Practices-green?logo=opensourcesecurity[OpenSSF Best Practices,link="https://www.bestpractices.dev/en/projects/new?repo_url=https://github.com/hyperpolymath/gossamer"] -image:https://img.shields.io/badge/License-PMPL--1.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] +image:https://img.shields.io/badge/License-MPL--2.0-blue.svg[License: PMPL-1.0,link="https://github.com/hyperpolymath/palimpsest-license"] image:https://img.shields.io/github/v/release/hyperpolymath/gossamer[Release,link="https://github.com/hyperpolymath/gossamer/releases"] image:https://img.shields.io/badge/FFI-Zig-orange.svg[Zig FFI] image:https://api.securityscorecards.dev/projects/github.com/hyperpolymath/gossamer/badge[OpenSSF Scorecard,link="https://securityscorecards.dev/viewer/?uri=github.com/hyperpolymath/gossamer"] diff --git a/ROADMAP.adoc b/ROADMAP.adoc index 288997b..4d910f4 100644 --- a/ROADMAP.adoc +++ b/ROADMAP.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Gossamer Webview Shell — Roadmap Gossamer is a linearly-typed webview shell built in Ephapax with Idris2 ABI diff --git a/SECURITY.md b/SECURITY.md index 1a29117..5c4d5e9 100644 --- a/SECURITY.md +++ b/SECURITY.md @@ -1,4 +1,4 @@ - + # Security Policy ## Reporting a Vulnerability diff --git a/TOPOLOGY.md b/TOPOLOGY.md index cdabca9..bab61cb 100644 --- a/TOPOLOGY.md +++ b/TOPOLOGY.md @@ -1,4 +1,4 @@ - + # TOPOLOGY.md — Gossamer diff --git a/android/README.adoc b/android/README.adoc index f68bfcb..9f4f050 100644 --- a/android/README.adoc +++ b/android/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Android :toc: macro diff --git a/android/gossamer-android-services/README.adoc b/android/gossamer-android-services/README.adoc index f7254e8..d627eb4 100644 --- a/android/gossamer-android-services/README.adoc +++ b/android/gossamer-android-services/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = gossamer-android-services :toc: macro diff --git a/android/gossamer-android-services/src/androidTest/README.adoc b/android/gossamer-android-services/src/androidTest/README.adoc index 17b7f94..ab3d18d 100644 --- a/android/gossamer-android-services/src/androidTest/README.adoc +++ b/android/gossamer-android-services/src/androidTest/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = gossamer-android-services — synthetic subclass tests :toc: macro diff --git a/api/README.adoc b/api/README.adoc index ba5c5a9..a063141 100644 --- a/api/README.adoc +++ b/api/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = API Public API surface for gossamer, currently exposing a zig binding (`v/gossamer.v`). This directory tracks the versioned stable interface that downstream consumers depend on; each subdirectory corresponds to a major API version. diff --git a/audits/audit-ffi-2026-05-26.md b/audits/audit-ffi-2026-05-26.md index ca040d4..c9318c1 100644 --- a/audits/audit-ffi-2026-05-26.md +++ b/audits/audit-ffi-2026-05-26.md @@ -1,5 +1,5 @@ diff --git a/benchmarks/README.adoc b/benchmarks/README.adoc index e774a62..5a4b8f4 100644 --- a/benchmarks/README.adoc +++ b/benchmarks/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Benchmarks Top-level benchmark entry-point scripts for gossamer. The `startup-bench.sh` script here drives high-level timing measurements; per-category benchmarks live under `tests/bench/`. diff --git a/bindings/README.adoc b/bindings/README.adoc index 587cb2e..eea44e3 100644 --- a/bindings/README.adoc +++ b/bindings/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Bindings Language-specific client bindings that wrap the gossamer C ABI for use from higher-level languages. Current targets are `rescript/` (ReScript/Deno) and `rust/` (Rust crate); each subdirectory is a self-contained build unit. diff --git a/bindings/affinescript/README.adoc b/bindings/affinescript/README.adoc index efbe9b2..ce65899 100644 --- a/bindings/affinescript/README.adoc +++ b/bindings/affinescript/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Gossamer AffineScript bindings :toc: macro diff --git a/cli/README.adoc b/cli/README.adoc index 109b3bb..7896b13 100644 --- a/cli/README.adoc +++ b/cli/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = CLI Zig command-line interface for gossamer, providing `gossamer` binary entry-point, file-watcher integration, and developer tooling. Build with `zig build` from this directory; the resulting binary is the primary way to launch and manage gossamer windows from the shell. diff --git a/cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc b/cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc index 1f83066..0d87048 100644 --- a/cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc +++ b/cli/launcher/docs/GTK-BLOCKING-DESIGN.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = gossamer_run, the GTK main loop, and wasmtime host bridges :toc: diff --git a/configs/README.adoc b/configs/README.adoc index eb154f5..76e9886 100644 --- a/configs/README.adoc +++ b/configs/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Configs Nickel configuration schemas and default values for gossamer runtime configuration. `config.ncl` defines the canonical schema; it is evaluated at build time to produce the JSON configs consumed by the gossamer binary. diff --git a/container/README.adoc b/container/README.adoc index a61b127..47389c7 100644 --- a/container/README.adoc +++ b/container/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = gossamer Container Templates :toc: left diff --git a/contractiles/README.adoc b/contractiles/README.adoc index f81a14b..e7924b8 100644 --- a/contractiles/README.adoc +++ b/contractiles/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Contractiles Machine-readable contractile definitions governing the obligations and constraints for gossamer across its build, trust, and intent lifecycle. Each subdirectory holds one contractile verb: `intend/` (north-star intent), `must/` (hard constraints), `trust/` (trust policy), and `k9/` (metadata service binding). diff --git a/deploy/README.adoc b/deploy/README.adoc index 3bd153f..c6ec133 100644 --- a/deploy/README.adoc +++ b/deploy/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Deploy Deployment artefacts and infrastructure-as-code for gossamer release pipelines. Place container orchestration files, cloud deployment manifests, and release automation scripts here as the project matures. diff --git a/docs/RSR_OUTLINE.adoc b/docs/RSR_OUTLINE.adoc index e07a65e..014b21c 100644 --- a/docs/RSR_OUTLINE.adoc +++ b/docs/RSR_OUTLINE.adoc @@ -281,7 +281,7 @@ This template is part of: == License -SPDX-License-Identifier: MPL-2.0 +SPDX-License-Identifier: CC-BY-SA-4.0 == Links diff --git a/docs/STATE-VISUALIZER.adoc b/docs/STATE-VISUALIZER.adoc index 422fcd5..2af3297 100644 --- a/docs/STATE-VISUALIZER.adoc +++ b/docs/STATE-VISUALIZER.adoc @@ -1,7 +1,7 @@ = Project State Visualizer [source] ---- - + diff --git a/docs/architecture/THREAT-MODEL.adoc b/docs/architecture/THREAT-MODEL.adoc index a9b8237..061fb18 100644 --- a/docs/architecture/THREAT-MODEL.adoc +++ b/docs/architecture/THREAT-MODEL.adoc @@ -1,5 +1,5 @@ = Threat Model - + # Threat Model: gossamer diff --git a/docs/architecture/android-components.adoc b/docs/architecture/android-components.adoc index 52c874f..bad5e07 100644 --- a/docs/architecture/android-components.adoc +++ b/docs/architecture/android-components.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = Gossamer Android: native component hosting :toc: macro diff --git a/docs/attribution/MAINTAINERS.adoc b/docs/attribution/MAINTAINERS.adoc index a1c6544..48d9781 100644 --- a/docs/attribution/MAINTAINERS.adoc +++ b/docs/attribution/MAINTAINERS.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Maintainers :toc: preamble diff --git a/docs/decisions/0000-template.adoc b/docs/decisions/0000-template.adoc index b1a561f..6710304 100644 --- a/docs/decisions/0000-template.adoc +++ b/docs/decisions/0000-template.adoc @@ -1,5 +1,5 @@ = Architecture Decision Record: 0000-template - + # [NUMBER]. [TITLE] diff --git a/docs/decisions/0001-adopt-rsr-standard.adoc b/docs/decisions/0001-adopt-rsr-standard.adoc index 7e54838..b5f8a1e 100644 --- a/docs/decisions/0001-adopt-rsr-standard.adoc +++ b/docs/decisions/0001-adopt-rsr-standard.adoc @@ -1,5 +1,5 @@ = Architecture Decision Record: 0001-adopt-rsr-standard - + # 1. Adopt Rhodium Standard Repository (RSR) Template diff --git a/docs/decisions/ADR-001-gossamer-webview-shell.adoc b/docs/decisions/ADR-001-gossamer-webview-shell.adoc index f974f1f..1b112e9 100644 --- a/docs/decisions/ADR-001-gossamer-webview-shell.adoc +++ b/docs/decisions/ADR-001-gossamer-webview-shell.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) :toc: macro :toclevels: 3 diff --git a/docs/developer/ABI-FFI-README.adoc b/docs/developer/ABI-FFI-README.adoc index 5bb86e5..357493e 100644 --- a/docs/developer/ABI-FFI-README.adoc +++ b/docs/developer/ABI-FFI-README.adoc @@ -1,5 +1,5 @@ = Gossamer ABI/FFI Documentation -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) == Overview diff --git a/docs/gossamer-conf-reference.adoc b/docs/gossamer-conf-reference.adoc index 91d7f86..19870a3 100644 --- a/docs/gossamer-conf-reference.adoc +++ b/docs/gossamer-conf-reference.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) = Gossamer Configuration Reference Jonathan D.A. Jewell diff --git a/docs/governance/CRG-AUDIT-2026-04-18.adoc b/docs/governance/CRG-AUDIT-2026-04-18.adoc index 784382f..a8ea35a 100644 --- a/docs/governance/CRG-AUDIT-2026-04-18.adoc +++ b/docs/governance/CRG-AUDIT-2026-04-18.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 // Copyright (c) 2026 Jonathan D.A. Jewell = Gossamer — CRG Audit (2026-04-18) diff --git a/docs/practice/AI-CONVENTIONS.adoc b/docs/practice/AI-CONVENTIONS.adoc index f0ed9ea..b0f765a 100644 --- a/docs/practice/AI-CONVENTIONS.adoc +++ b/docs/practice/AI-CONVENTIONS.adoc @@ -1,5 +1,5 @@ = AI Conventions - + # AI Conventions (Authoritative Source) @@ -23,7 +23,7 @@ Per-tool config files (.cursorrules, .clinerules, etc.) reference this document. - Fallback (platform-required only): MPL-2.0 with comment explaining why. - NEVER use AGPL-3.0. - Preserve third-party licenses verbatim. -- Every source file needs `# SPDX-License-Identifier: MPL-2.0`. +- Every source file needs `# SPDX-License-Identifier: CC-BY-SA-4.0`. ## Author Attribution diff --git a/docs/practice/STATE-VISUALIZER-GUIDE.adoc b/docs/practice/STATE-VISUALIZER-GUIDE.adoc index c2490ca..835db9c 100644 --- a/docs/practice/STATE-VISUALIZER-GUIDE.adoc +++ b/docs/practice/STATE-VISUALIZER-GUIDE.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = TOPOLOGY.md — Generation Guide Jonathan D.A. Jewell (hyperpolymath) :toc: diff --git a/docs/tech-debt-2026-05-26.md b/docs/tech-debt-2026-05-26.md index a6f7376..14b1193 100644 --- a/docs/tech-debt-2026-05-26.md +++ b/docs/tech-debt-2026-05-26.md @@ -1,5 +1,5 @@ diff --git a/docs/templates/contractiles/README.adoc b/docs/templates/contractiles/README.adoc index 121da7a..4eeac6b 100644 --- a/docs/templates/contractiles/README.adoc +++ b/docs/templates/contractiles/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Contractile Templates Blank templates for projects that want to replace the hyperpolymath diff --git a/docs/wikis/Home.md b/docs/wikis/Home.md index 48cbf8d..ad34f2d 100644 --- a/docs/wikis/Home.md +++ b/docs/wikis/Home.md @@ -1,4 +1,4 @@ - + # Gossamer **Build desktop apps that can't leak resources. By design, not by discipline.** diff --git a/ffi/README.adoc b/ffi/README.adoc index 08f599c..2826774 100644 --- a/ffi/README.adoc +++ b/ffi/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = FFI Zig FFI implementation providing the C-compatible ABI bridge between the Idris2 interface definitions and the native WebView platform code. The `zig/` subdirectory contains the Zig build unit; generated C headers consumed here live in `generated/`. diff --git a/generated/README.adoc b/generated/README.adoc index 1cd493b..8da743a 100644 --- a/generated/README.adoc +++ b/generated/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Generated Auto-generated artefacts produced by tooling during the build or verification pipeline — do not edit by hand. diff --git a/packaging/README.adoc b/packaging/README.adoc index e6b7458..61169b7 100644 --- a/packaging/README.adoc +++ b/packaging/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Packaging Platform-specific packaging recipes for distributing gossamer to end users. Subdirectories cover `debian/` (APT), `flatpak/` (Flatpak/Flathub), `macos/` (notarised DMG), `rpm/` (RPM spec), and `windows/` (WiX installer). diff --git a/schema/README.adoc b/schema/README.adoc index fed8ae2..07bb957 100644 --- a/schema/README.adoc +++ b/schema/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Schema JSON Schema definitions for gossamer's runtime configuration and Groove manifest formats. `gossamer.conf.schema.json` validates `gossamer.conf.json`; `groove-manifest.schema.json` validates Groove service manifests consumed by gossamer. diff --git a/schemas/README.adoc b/schemas/README.adoc index 0aace4a..de34264 100644 --- a/schemas/README.adoc +++ b/schemas/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Schemas CUE-language schema definitions used to validate and type-check gossamer's Nickel configurations. `config.cue` is the canonical CUE schema; it cross-validates with `configs/config.ncl` to ensure both schema languages agree on the configuration surface. diff --git a/scripts/README.adoc b/scripts/README.adoc index 3384928..fc35eae 100644 --- a/scripts/README.adoc +++ b/scripts/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Scripts Developer and build utility scripts for gossamer. Includes desktop integration installation (`install-desktop.sh`), Markdown-to-HTML conversion (`md-to-html.awk`), a Zig-based static site build runner (`ssg-build-runner.zig`), a template substitution helper (`template-sub.awk`), and a headless-display test wrapper (`test-with-display.sh`). diff --git a/site/README.adoc b/site/README.adoc index cedead3..bd6f180 100644 --- a/site/README.adoc +++ b/site/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Site Static website sources for the gossamer project homepage. Contains `index.html`, `style.css`, a `src/` subtree for additional page content, and a dev.to announcement draft; built by `scripts/ssg-build-runner.zig`. diff --git a/src/interface/Gossamer/ABI/AndroidComponents.idr b/src/interface/Gossamer/ABI/AndroidComponents.idr deleted file mode 120000 index d3c5817..0000000 --- a/src/interface/Gossamer/ABI/AndroidComponents.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/AndroidComponents.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/AndroidComponents.idr b/src/interface/Gossamer/ABI/AndroidComponents.idr new file mode 100644 index 0000000..d707342 --- /dev/null +++ b/src/interface/Gossamer/ABI/AndroidComponents.idr @@ -0,0 +1,293 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Android Non-UI Component Lifecycles for Gossamer (GS-ANDROID) +||| +||| Gossamer hosts a WebView in an Activity, but a production Android app also +||| needs background components with no webview in scope: a foreground Service, +||| a BroadcastReceiver, and an AppWidgetProvider. This module gives those +||| components the same formal treatment the webview already enjoys: +||| +||| 1. Each component is a state machine with a TERMINAL teardown state and +||| no transition out of it (mirrors WindowStateMachine's `Closed`). +||| 2. Event dispatch is only well-typed while the component is LIVE — the +||| type-level analogue of the runtime plugin-liveness check that prevents +||| use-after-free in the IPC dispatcher. +||| 3. The long-lived Service is modelled as a `LinearHandle` over the SAME +||| lifecycle framework as the webview (HandleLinearity), so the linear +||| "consume exactly once" guarantee crosses the new JNI boundary intact. +||| +||| The native side of these contracts lives in src/interface/ffi/src/ +||| android_{service,receiver,widget}.zig; the JVM side is gossamer-GENERATED +||| Java (android/generated/). An app binds pure handlers via the +||| gossamer_{service,receiver,widget}_bind FFI declared at the foot of this +||| module and never touches JNI itself. +||| +||| OPEN (tracked as a gossamer issue): the deep region-calculus question of how +||| a long-lived, JVM-owned Service handle relates to the shorter-lived webview +||| region — and how cross-region references (a Service pushing a Widget update) +||| are tracked — is NOT settled here. This module proves the parts that are +||| unambiguous (terminal teardown, dispatch-only-while-live, single-consume) +||| and leaves the region-nesting design to that issue. +||| +||| No unsafe escape hatches; every proof is constructive. + +module Gossamer.ABI.AndroidComponents + +import Gossamer.ABI.Types +import Gossamer.ABI.HandleLinearity +import Data.So + +%default total + +-------------------------------------------------------------------------------- +-- Component Taxonomy +-------------------------------------------------------------------------------- + +||| The three non-UI Android components Gossamer hosts natively. +public export +data ComponentKind = ServiceC | ReceiverC | WidgetC + +||| Whether a component owns a LONG-LIVED handle (one whose lifetime spans many +||| dispatches) versus a TRANSIENT one (constructed per dispatch by the JVM). +||| +||| Only the Service owns a long-lived handle: the JVM keeps the Service object +||| alive across many onStartCommand calls. A BroadcastReceiver and an +||| AppWidgetProvider update are constructed, called once, and discarded — each +||| dispatch is a scoped borrow, not an owned handle. +public export +data LongLived : ComponentKind -> Type where + ServiceIsLongLived : LongLived ServiceC + +||| Receiver dispatch is transient (no owned long-lived handle). +public export +data Transient : ComponentKind -> Type where + ReceiverIsTransient : Transient ReceiverC + WidgetIsTransient : Transient WidgetC + +||| Long-lived and transient are disjoint classifications. +public export +longLivedNotTransient : LongLived k -> Transient k -> Void +longLivedNotTransient ServiceIsLongLived x = case x of {} + +-------------------------------------------------------------------------------- +-- Foreground Service lifecycle: Created -> Started* -> Destroyed +-------------------------------------------------------------------------------- + +||| States of a gossamer-hosted foreground Service. +||| Mirrors android.app.Service: onCreate, onStartCommand (repeatable), +||| onDestroy (terminal). +public export +data SvcState = SvcCreated | SvcStarted | SvcDestroyed + +||| Service lifecycle operations (the JNI entry points in services_android.zig). +public export +data SvcOp = OnCreate | OnStartCommand | OnDestroy + +||| Valid Service transitions. No constructor has source SvcDestroyed, so +||| SvcDestroyed is absorbing. onStartCommand may fire repeatedly (START_STICKY +||| redelivery), modelled by the Started -> Started self-loop. +public export +data SvcTransition : (s : SvcState) -> (op : SvcOp) -> (t : SvcState) -> Type where + StartFromCreated : SvcTransition SvcCreated OnStartCommand SvcStarted + StartFromStarted : SvcTransition SvcStarted OnStartCommand SvcStarted + DestroyFromCreated : SvcTransition SvcCreated OnDestroy SvcDestroyed + DestroyFromStarted : SvcTransition SvcStarted OnDestroy SvcDestroyed + +||| GS-ANDROID-INV-1: onDestroy is terminal — no transition leaves SvcDestroyed. +public export +svcDestroyedTerminal : SvcTransition SvcDestroyed op t -> Void +svcDestroyedTerminal _ impossible + +||| A Service is "live" (safe to dispatch events into) iff it is not destroyed. +public export +data SvcLive : SvcState -> Type where + LiveCreated : SvcLive SvcCreated + LiveStarted : SvcLive SvcStarted + +||| A destroyed Service is not live (no dispatch after teardown). +public export +svcDestroyedNotLive : SvcLive SvcDestroyed -> Void +svcDestroyedNotLive x = case x of {} + +||| onStartCommand always lands in the Started state — the foreground work is +||| running regardless of whether this was the first start or a redelivery. +public export +startCommandStarts : SvcTransition s OnStartCommand t -> t = SvcStarted +startCommandStarts StartFromCreated = Refl +startCommandStarts StartFromStarted = Refl + +||| onDestroy always lands in the terminal state. +public export +destroyDestroys : SvcTransition s OnDestroy t -> t = SvcDestroyed +destroyDestroys DestroyFromCreated = Refl +destroyDestroys DestroyFromStarted = Refl + +-------------------------------------------------------------------------------- +-- BroadcastReceiver lifecycle: Live -> Complete (one-shot) +-------------------------------------------------------------------------------- + +||| States of a single BroadcastReceiver invocation. The JVM constructs the +||| receiver, calls onReceive exactly once, and discards it; onReceive must +||| complete within its window (Android tears the receiver down on return). +public export +data RcvState = RcvLive | RcvComplete + +||| The single valid receiver transition: handle the broadcast, then complete. +public export +data RcvTransition : (s : RcvState) -> (t : RcvState) -> Type where + ReceiveOnce : RcvTransition RcvLive RcvComplete + +||| GS-ANDROID-INV-2: a completed receiver is terminal — onReceive cannot fire +||| twice on the same instance. +public export +rcvCompleteTerminal : RcvTransition RcvComplete t -> Void +rcvCompleteTerminal _ impossible + +-------------------------------------------------------------------------------- +-- AppWidgetProvider lifecycle: Enabled -> Disabled (updates are borrows) +-------------------------------------------------------------------------------- + +||| States of a gossamer-hosted home-screen widget provider. onEnabled fires +||| when the first instance is placed; onDisabled when the last is removed +||| (terminal). onUpdate is a BORROW: it renders without changing provider +||| state, exactly like the webview's loadHTML/navigate borrows. +public export +data WdgState = WdgEnabled | WdgDisabled + +public export +data WdgOp = WidgetOnUpdate | WidgetOnDisabled + +||| Valid widget transitions. onUpdate is absent here because, as a borrow, it +||| does not move the provider between states (see `widgetUpdateBorrow`). +public export +data WdgTransition : (s : WdgState) -> (op : WdgOp) -> (t : WdgState) -> Type where + DisableFromEnabled : WdgTransition WdgEnabled WidgetOnDisabled WdgDisabled + +||| GS-ANDROID-INV-3: onDisabled is terminal. +public export +wdgDisabledTerminal : WdgTransition WdgDisabled op t -> Void +wdgDisabledTerminal _ impossible + +||| onUpdate is a borrow: it is only valid on an enabled provider and leaves the +||| state unchanged. Encoded as a predicate rather than a state transition. +public export +data WidgetUpdateBorrow : WdgState -> Type where + UpdateWhileEnabled : WidgetUpdateBorrow WdgEnabled + +||| A disabled provider cannot service updates. +public export +wdgDisabledNoUpdate : WidgetUpdateBorrow WdgDisabled -> Void +wdgDisabledNoUpdate x = case x of {} + +-------------------------------------------------------------------------------- +-- Service as a Linear Handle (linearity preserved across the JNI boundary) +-------------------------------------------------------------------------------- + +||| Opaque handle to a gossamer-hosted foreground Service. +||| Like WebviewHandle, this is a LINEAR resource carrying a non-null proof: +||| it is allocated once (onCreate) and consumed once (onDestroy). +public export +data ServiceHandle : Type where + MkService : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> ServiceHandle + +||| Extract the raw pointer (for FFI calls). +public export +servicePtr : ServiceHandle -> Bits64 +servicePtr (MkService ptr) = ptr + +||| Recover the erased non-null witness as a ValidToken, mirroring +||| HandleLinearity.webviewValid. The witness already lives inside MkService; +||| this re-exposes it so allocation is total with no runtime null re-check. +public export +serviceValid : (s : ServiceHandle) -> ValidToken (servicePtr s) +serviceValid (MkService ptr {nonNull}) = MkValid {nonNull} + +||| A linearly-tracked Service handle, reusing the generic Allocated/Active/ +||| Consumed machine from HandleLinearity. This is the load-bearing claim that +||| the new Service boundary keeps Gossamer's linear guarantees: a Service that +||| is leaked (never onDestroy) or torn down twice does not type-check. +public export +LinearService : HandleState -> Type +LinearService = LinearHandle ServiceHandle + +||| Allocate a linear Service handle (state Allocated), set up at onCreate. +public export +allocateService : ServiceHandle -> LinearService Allocated +allocateService s = MkLinear s (servicePtr s) {valid = serviceValid s} + +||| Consume the Service handle at onDestroy. Active -> Consumed, returning the +||| raw handle for the final FFI teardown call. There is no way to reconstruct +||| an Active handle from the Consumed one, so no dispatch can follow. +public export +consumeForStop : LinearService Active -> (ServiceHandle, LinearService Consumed) +consumeForStop = consume + +||| The Service lifecycle state maps onto the generic handle lifecycle: +||| Created↔Allocated, Started↔Active, Destroyed↔Consumed. +public export +svcToHandleState : SvcState -> HandleState +svcToHandleState SvcCreated = Allocated +svcToHandleState SvcStarted = Active +svcToHandleState SvcDestroyed = Consumed + +||| The mapping sends the terminal Service state to the terminal handle state, +||| witnessing that "Service destroyed" and "handle consumed" coincide. +public export +destroyedIsConsumed : svcToHandleState SvcDestroyed = Consumed +destroyedIsConsumed = Refl + +-------------------------------------------------------------------------------- +-- FFI: native callback registration (implemented in services_android.zig) +-------------------------------------------------------------------------------- +-- +-- The #71 companion uses the subclass model: the JVM-side base classes +-- (io.gossamer.services.*) own the Android contracts, and the app's native core +-- (Rust/Zig) plugs in by registering plain C callbacks at JNI_OnLoad. gossamer +-- owns every JNI call. Each callback is a raw C function pointer (Bits64); the +-- concrete handler is supplied by the app, so these declarations fix only the C +-- symbol and arity. The foreground-Service handle threaded to the callbacks is +-- the independent ServiceHandle modelled above. + +||| Register the foreground-Service callbacks: create, startCommand, destroy, +||| sensorEvent (four raw C function pointers). +export +%foreign "C:gossamer_android_register_service_callbacks, libgossamer" +prim__registerServiceCallbacks : Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO () + +||| Register the AppWidget callbacks: fetchState, handleAction. +export +%foreign "C:gossamer_android_register_widget_callbacks, libgossamer" +prim__registerWidgetCallbacks : Bits64 -> Bits64 -> PrimIO () + +||| Register the boot-receiver shouldRestart predicate callback. +export +%foreign "C:gossamer_android_register_boot_callback, libgossamer" +prim__registerBootCallback : Bits64 -> PrimIO () + +||| Register the Activity intent callback. +export +%foreign "C:gossamer_android_register_intent_callback, libgossamer" +prim__registerIntentCallback : Bits64 -> PrimIO () + +||| Safe wrapper: register the foreground-Service native callbacks. +export +registerServiceCallbacks : (create : Bits64) -> (start : Bits64) -> (destroy : Bits64) -> (sensor : Bits64) -> IO () +registerServiceCallbacks c s d sn = primIO (prim__registerServiceCallbacks c s d sn) + +||| Safe wrapper: register the AppWidget native callbacks. +export +registerWidgetCallbacks : (fetchState : Bits64) -> (handleAction : Bits64) -> IO () +registerWidgetCallbacks f h = primIO (prim__registerWidgetCallbacks f h) + +||| Safe wrapper: register the boot-receiver callback. +export +registerBootCallback : (shouldRestart : Bits64) -> IO () +registerBootCallback sr = primIO (prim__registerBootCallback sr) + +||| Safe wrapper: register the Activity intent callback. +export +registerIntentCallback : (onIntent : Bits64) -> IO () +registerIntentCallback oi = primIO (prim__registerIntentCallback oi) diff --git a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr deleted file mode 120000 index c75570c..0000000 --- a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/CapabilityAuthenticity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr new file mode 100644 index 0000000..a591ce0 --- /dev/null +++ b/src/interface/Gossamer/ABI/CapabilityAuthenticity.idr @@ -0,0 +1,234 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Capability Authenticity Proofs for Gossamer +||| +||| Proves that declared capabilities match actual behaviour. +||| A service cannot claim to offer a capability it does not implement, +||| and a consumer cannot invoke a capability the service does not offer. +||| +||| Builds on the Groove.idr capability sets and the Cap type from Types.idr. +||| +||| Key properties proved: +||| 1. Declaration-implementation correspondence: every declared capability +||| has a corresponding handler implementation. +||| 2. No phantom capabilities: you cannot invoke an undeclared capability. +||| 3. Capability attenuation: delegated capabilities cannot exceed the +||| original grant scope. +||| 4. Revocation completeness: revoking a capability removes all derived +||| capabilities. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.CapabilityAuthenticity + +import Gossamer.ABI.Types +import Gossamer.ABI.Groove +import Data.So +import Data.Bits +import Data.List +import Data.List.Elem + +%default total + +-------------------------------------------------------------------------------- +-- Capability Implementation Witness +-------------------------------------------------------------------------------- + +||| A handler for a specific capability type. +||| +||| This is an opaque witness that a capability has been implemented. +||| The actual handler lives in the Zig FFI layer; this type is the +||| compile-time proof that an implementation exists. +||| +||| The phantom type parameter `cap` ties the handler to a specific +||| capability, preventing capability confusion. +public export +data CapHandler : (cap : CapabilityType) -> Type where + ||| Witness that a handler exists for the given capability. + ||| The Bits64 is the handler's function pointer at the FFI level. + MkHandler : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> CapHandler cap + +||| Extract handler pointer (for FFI calls). +public export +handlerPtr : CapHandler cap -> Bits64 +handlerPtr (MkHandler ptr) = ptr + +-------------------------------------------------------------------------------- +-- Implementation Table +-------------------------------------------------------------------------------- + +||| A table mapping declared capabilities to their handler implementations. +||| +||| Parameterised by the capability set, ensuring that every declared +||| capability has a corresponding handler. +public export +data ImplTable : (caps : CapSet) -> Type where + ||| Empty implementation table (no capabilities). + ITNil : ImplTable [] + ||| A handler for `cap` plus implementations for the rest. + ITCons : CapHandler cap + -> ImplTable rest + -> ImplTable (cap :: rest) + +||| Look up a handler for a specific capability in the implementation table. +||| Requires a proof that the capability is in the declared set. +public export +lookupHandler : ImplTable caps -> Elem cap caps -> CapHandler cap +lookupHandler (ITCons handler _) Here = handler +lookupHandler (ITCons _ rest) (There later) = lookupHandler rest later + +-------------------------------------------------------------------------------- +-- Declaration-Implementation Correspondence +-------------------------------------------------------------------------------- + +||| Proof that a groove manifest's declared capabilities are fully implemented. +||| +||| This is the core authenticity guarantee: a service that declares +||| capabilities [Voice, Text, Presence] must provide handlers for all three. +||| The ImplTable type enforces this by construction — you cannot build an +||| ImplTable unless you supply a handler for every element. +public export +data FullyImplemented : (offers : CapSet) -> Type where + ||| Witness that every offered capability has a handler. + MkFullyImplemented : ImplTable offers -> FullyImplemented offers + +||| Construct a fully-implemented proof from an implementation table. +public export +proveImplemented : ImplTable offers -> FullyImplemented offers +proveImplemented = MkFullyImplemented + +-------------------------------------------------------------------------------- +-- No Phantom Capabilities +-------------------------------------------------------------------------------- + +||| Proof that invoking a capability requires it to be declared. +||| +||| A consumer cannot call a capability that is not in the service's +||| offers set. The Elem proof is the compile-time guarantee. +public export +data InvocationPermit : (cap : CapabilityType) -> (offers : CapSet) -> Type where + ||| You may invoke `cap` because it appears in the offers set. + MkPermit : Elem cap offers -> InvocationPermit cap offers + +||| Attempt to create an invocation permit. +||| Fails at compile time if cap is not in offers (via the auto-search +||| for Elem cap offers). +public export +permitInvocation : {auto prf : Elem cap offers} -> InvocationPermit cap offers +permitInvocation = MkPermit prf + +||| Invoke a capability with both authenticity and permit checks. +||| Requires: +||| 1. The capability set is fully implemented (no phantom handlers) +||| 2. The specific capability is in the offers set (no phantom invocations) +public export +authenticInvoke : FullyImplemented offers + -> InvocationPermit cap offers + -> CapHandler cap +authenticInvoke (MkFullyImplemented table) (MkPermit elem) = + lookupHandler table elem + +-------------------------------------------------------------------------------- +-- Capability Attenuation +-------------------------------------------------------------------------------- + +||| A derived capability that is a subset of an original grant. +||| +||| When a capability is delegated (e.g. a panel receives a scoped +||| capability from the shell), the derived capability cannot exceed +||| the original. Attenuation guarantees that delegation is safe. +public export +data Attenuated : (original : ResourceKind) -> (derived : ResourceKind) -> Type where + ||| Identity attenuation: the derived capability is the same as the original. + ||| This is the base case for direct grants. + AttSame : Attenuated r r + ||| Filesystem read-only is an attenuation of read-write. + AttFsReadOnly : Attenuated (FileSystem (ReadWrite paths)) + (FileSystem (ReadOnlyPaths paths)) + ||| Filesystem AppData is an attenuation of any filesystem scope. + AttFsAppData : Attenuated (FileSystem scope) (FileSystem AppData) + ||| Network: specific hosts is an attenuation of all-network. + AttNetHosts : Attenuated (Network AllNetwork) (Network (AllowHosts hosts)) + ||| Shell: specific commands is an attenuation of all-shell. + AttShellCmds : Attenuated (Shell AllShell) (Shell (AllowCommands cmds)) + ||| Groove: specific targets is an attenuation of all-groove. + AttGrooveTargets : Attenuated (Groove AllGroove) (Groove (AllowTargets targets)) + +||| Proof that attenuation is transitive. +||| If A attenuates to B and B attenuates to C, then A attenuates to C. +||| We prove this for the identity case; other cases are encoded directly +||| in the Attenuated constructors. +public export +attenuateTransitive : Attenuated a b -> Attenuated b b -> Attenuated a b +attenuateTransitive prf AttSame = prf +-- `AttFsAppData : Attenuated (FileSystem scope) (FileSystem AppData)` also +-- inhabits `Attenuated b b` (when scope = AppData), so coverage requires it. +-- `b` is then `FileSystem AppData` and `prf : Attenuated a b` is the result. +attenuateTransitive prf AttFsAppData = prf + +-------------------------------------------------------------------------------- +-- Revocation Completeness +-------------------------------------------------------------------------------- + +||| A revocation token tracks which capabilities have been revoked. +public export +data RevocationSet : Type where + ||| No capabilities revoked. + RevEmpty : RevocationSet + ||| A capability token has been revoked. + RevAdd : (token : Bits64) -> RevocationSet -> RevocationSet + +||| Proof that a capability token is in the revocation set. +public export +data IsRevoked : (token : Bits64) -> RevocationSet -> Type where + ||| The token is the most recently revoked. + RevokedHere : IsRevoked token (RevAdd token rest) + ||| The token was revoked earlier. + RevokedThere : IsRevoked token rest -> IsRevoked token (RevAdd other rest) + +||| Proof that a derived capability is revoked when its parent is revoked. +||| +||| If capability A was delegated to produce capability B (via attenuation), +||| and A's token is revoked, then B is also invalid. +public export +data RevocationComplete : Type where + ||| Witness that revoking parent token invalidates derived token. + MkRevComplete : (parentToken : Bits64) + -> (derivedToken : Bits64) + -> (revoked : RevocationSet) + -> {auto 0 parentRevoked : IsRevoked parentToken revoked} + -> RevocationComplete + +-------------------------------------------------------------------------------- +-- Groove Manifest Authenticity +-------------------------------------------------------------------------------- + +||| Proof that a groove manifest is authentic: every offered capability +||| is implemented and every consumed capability is actually needed. +||| +||| This combines: +||| 1. FullyImplemented for the offers set +||| 2. A witness that the consumes set is referenced by at least one handler +public export +data AuthenticManifest : (offers : CapSet) -> (consumes : CapSet) -> Type where + MkAuthentic : FullyImplemented offers + -> AuthenticManifest offers consumes + +||| Construct an authentic manifest proof. +public export +proveAuthentic : ImplTable offers -> AuthenticManifest offers consumes +proveAuthentic table = MkAuthentic (proveImplemented table) + +||| Proof that connecting to an authentic service is safe. +||| +||| If the service's manifest is authentic (all declared capabilities are +||| implemented) and compatible (our requirements are satisfied), then +||| the connection will behave as advertised. +public export +data SafeConnection : (clientReqs : CapSet) -> (serverOffers : CapSet) -> Type where + MkSafe : AuthenticManifest serverOffers serverCons + -> IsSubset clientReqs serverOffers + -> SafeConnection clientReqs serverOffers diff --git a/src/interface/Gossamer/ABI/Foreign.idr b/src/interface/Gossamer/ABI/Foreign.idr deleted file mode 120000 index e9dcedb..0000000 --- a/src/interface/Gossamer/ABI/Foreign.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/Foreign.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Foreign.idr b/src/interface/Gossamer/ABI/Foreign.idr new file mode 100644 index 0000000..5f04e3f --- /dev/null +++ b/src/interface/Gossamer/ABI/Foreign.idr @@ -0,0 +1,215 @@ +||| SPDX-License-Identifier: MPL-2.0 +||| Foreign Function Interface Declarations for GOSSAMER +||| +||| This module declares all C-compatible functions that will be +||| implemented in the Zig FFI layer. +||| +||| All functions are declared here with type signatures and safety proofs. +||| Implementations live in ffi/zig/ + +module Gossamer.ABI.Foreign + +import Gossamer.ABI.Types +import Gossamer.ABI.Layout + +%default total + +-------------------------------------------------------------------------------- +-- Library Lifecycle +-------------------------------------------------------------------------------- + +||| Initialize the library +||| Returns a handle to the library instance, or Nothing on failure +export +%foreign "C:gossamer_init, libgossamer" +prim__init : PrimIO Bits64 + +||| Safe wrapper for library initialization +||| Requires a MainThreadProof witness — the library handle is main-thread-bound. +export +init : {auto prf : MainThreadProof} -> IO (Maybe WebviewHandle) +init = do + ptr <- primIO prim__init + pure (createWebview ptr) + +||| Clean up library resources +export +%foreign "C:gossamer_free, libgossamer" +prim__free : Bits64 -> PrimIO () + +||| Safe wrapper for cleanup +export +free : WebviewHandle -> IO () +free h = primIO (prim__free (webviewPtr h)) + +-------------------------------------------------------------------------------- +-- Core Operations +-------------------------------------------------------------------------------- + +||| Example operation: process data +export +%foreign "C:gossamer_process, libgossamer" +prim__process : Bits64 -> Bits32 -> PrimIO Bits32 + +||| Safe wrapper with error handling +export +process : WebviewHandle -> Bits32 -> IO (Either Result Bits32) +process h input = do + result <- primIO (prim__process (webviewPtr h) input) + pure $ case result of + 0 => Left Error + n => Right n + +-------------------------------------------------------------------------------- +-- String Operations +-------------------------------------------------------------------------------- + +||| Convert C string to Idris String +export +%foreign "support:idris2_getString, libidris2_support" +prim__getString : Bits64 -> String + +||| Free C string +export +%foreign "C:gossamer_free_string, libgossamer" +prim__freeString : Bits64 -> PrimIO () + +||| Get string result from library +export +%foreign "C:gossamer_get_string, libgossamer" +prim__getResult : Bits64 -> PrimIO Bits64 + +||| Safe string getter +export +getString : WebviewHandle -> IO (Maybe String) +getString h = do + ptr <- primIO (prim__getResult (webviewPtr h)) + if ptr == 0 + then pure Nothing + else do + let str = prim__getString ptr + primIO (prim__freeString ptr) + pure (Just str) + +-------------------------------------------------------------------------------- +-- Array/Buffer Operations +-------------------------------------------------------------------------------- + +||| Process array data +export +%foreign "C:gossamer_process_array, libgossamer" +prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32 + +||| Safe array processor +export +processArray : WebviewHandle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ()) +processArray h buf len = do + result <- primIO (prim__processArray (webviewPtr h) buf len) + pure $ case resultFromInt result of + Just Ok => Right () + Just err => Left err + Nothing => Left Error + where + resultFromInt : Bits32 -> Maybe Result + resultFromInt 0 = Just Ok + resultFromInt 1 = Just Error + resultFromInt 2 = Just InvalidParam + resultFromInt 3 = Just OutOfMemory + resultFromInt 4 = Just NullPointer + resultFromInt _ = Nothing + +-------------------------------------------------------------------------------- +-- Error Handling +-------------------------------------------------------------------------------- + +||| Get last error message +export +%foreign "C:gossamer_last_error, libgossamer" +prim__lastError : PrimIO Bits64 + +||| Retrieve last error as string +export +lastError : IO (Maybe String) +lastError = do + ptr <- primIO prim__lastError + if ptr == 0 + then pure Nothing + else pure (Just (prim__getString ptr)) + +-- errorDescription is re-exported via Gossamer.ABI.Types + +-------------------------------------------------------------------------------- +-- Version Information +-------------------------------------------------------------------------------- + +||| Get library version +export +%foreign "C:gossamer_version, libgossamer" +prim__version : PrimIO Bits64 + +||| Get version as string +export +version : IO String +version = do + ptr <- primIO prim__version + pure (prim__getString ptr) + +||| Get library build info +export +%foreign "C:gossamer_build_info, libgossamer" +prim__buildInfo : PrimIO Bits64 + +||| Get build information +export +buildInfo : IO String +buildInfo = do + ptr <- primIO prim__buildInfo + pure (prim__getString ptr) + +-------------------------------------------------------------------------------- +-- Callback Support +-------------------------------------------------------------------------------- + +||| Callback function type (C ABI) +public export +Callback : Type +Callback = Bits64 -> Bits32 -> Bits32 + +||| Register a callback. +||| The callback is passed to C as a function pointer: Idris2's C FFI +||| marshals the `Callback` closure directly (the prior `AnyPtr` + +||| `cast` had no `Cast Callback AnyPtr` instance and never compiled — +||| a latent error masked by the never-built module). +export +%foreign "C:gossamer_register_callback, libgossamer" +prim__registerCallback : Bits64 -> Callback -> PrimIO Bits32 + +||| Safe callback registration +export +registerCallback : WebviewHandle -> Callback -> IO (Either Result ()) +registerCallback h cb = do + result <- primIO (prim__registerCallback (webviewPtr h) cb) + pure $ case resultFromInt result of + Just Ok => Right () + Just err => Left err + Nothing => Left Error + where + resultFromInt : Bits32 -> Maybe Result + resultFromInt 0 = Just Ok + resultFromInt _ = Just Error + +-------------------------------------------------------------------------------- +-- Utility Functions +-------------------------------------------------------------------------------- + +||| Check if library is initialized +export +%foreign "C:gossamer_is_initialized, libgossamer" +prim__isInitialized : Bits64 -> PrimIO Bits32 + +||| Check initialization status +export +isInitialized : WebviewHandle -> IO Bool +isInitialized h = do + result <- primIO (prim__isInitialized (webviewPtr h)) + pure (result /= 0) diff --git a/src/interface/Gossamer/ABI/Groove.idr b/src/interface/Gossamer/ABI/Groove.idr deleted file mode 120000 index 90298de..0000000 --- a/src/interface/Gossamer/ABI/Groove.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/Groove.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Groove.idr b/src/interface/Gossamer/ABI/Groove.idr new file mode 100644 index 0000000..6453fe1 --- /dev/null +++ b/src/interface/Gossamer/ABI/Groove.idr @@ -0,0 +1,527 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Gossamer Groove — Type-Safe Composable Service Discovery +||| +||| A "groove" is a bidirectional capability interface between two systems. +||| Each system works standalone but enhances the other when co-present. +||| Grooves are panel-optional: they work headless, but CAN power PanLL panels. +||| +||| The dependent type system guarantees: +||| 1. Safe connect — you cannot connect unless required capabilities are met +||| 2. Safe disconnect — linear types enforce proper cleanup (no dangling grooves) +||| 3. Safe compose — chaining grooves is provably sound +||| 4. No phantom capabilities — you cannot claim what you do not implement +||| +||| Architecture: +||| GrooveManifest — declares offered/consumed capabilities (plain value) +||| GrooveHandle — linear resource proving a live connection +||| GrooveComposition — proof that two grooves can be composed +||| +||| Discovery: services expose GET /.well-known/groove on their port. +||| The Zig FFI layer (groove.zig) probes these and constructs handles. +||| +||| This extends the existing Cap/ResourceKind pattern to inter-service +||| boundaries. Where Cap gates operations within a Gossamer app, +||| GrooveHandle gates operations between Gossamer and external services. + +module Gossamer.ABI.Groove + +import Gossamer.ABI.Types +import Data.So +import Data.List +import Data.List.Elem +import Data.Bits + +%default total + +-------------------------------------------------------------------------------- +-- Capability Types +-------------------------------------------------------------------------------- + +||| Standard capability types that groove services can offer or consume. +||| Each type corresponds to a well-defined protocol interface. +public export +data CapabilityType : Type where + ||| WebRTC voice channels (Burble) + Voice : CapabilityType + ||| Real-time text messaging (Burble) + Text : CapabilityType + ||| User presence and speaking indicators (Burble) + Presence : CapabilityType + ||| Positional audio for spatial environments (Burble) + SpatialAudio : CapabilityType + ||| Server-side voice recording (Burble) + Recording : CapabilityType + ||| Text-to-speech synthesis (Burble) + TTS : CapabilityType + ||| Speech-to-text transcription (Burble) + STT : CapabilityType + ||| Cryptographic hash chain verification (Vext) + Integrity : CapabilityType + ||| Chronological feed verification (Vext) + FeedVerify : CapabilityType + ||| Merkle tree operations (Vext) + HashChain : CapabilityType + ||| Digital signature attestation (Vext/Avow) + Attestation : CapabilityType + ||| 8-modal entity storage (VeriSimDB) + OctadStorage : CapabilityType + ||| Cross-modal drift detection (VeriSimDB) + DriftDetection : CapabilityType + ||| Temporal version tracking (VeriSimDB) + TemporalVer : CapabilityType + ||| Neurosymbolic security scanning (Hypatia) + Scanning : CapabilityType + ||| Panel-based UI (PanLL) + PanelUI : CapabilityType + ||| Bot orchestration (gitbot-fleet) + BotOrch : CapabilityType + ||| Workflow automation (RPA Elysium) + Workflow : CapabilityType + ||| DNS record verification (rrecord-verity) + DNSVerify : CapabilityType + ||| Configuration orchestration (conflow) + ConfigOrch : CapabilityType + ||| Static analysis (panic-attacker) + StaticAnalysis : CapabilityType + ||| Theorem proving (ECHIDNA) + TheoremProve : CapabilityType + ||| Custom capability (extensible) + Custom : (name : String) -> CapabilityType + +||| Decidable equality for CapabilityType. +||| Required for Subset proofs. +public export +Eq CapabilityType where + Voice == Voice = True + Text == Text = True + Presence == Presence = True + SpatialAudio == SpatialAudio = True + Recording == Recording = True + TTS == TTS = True + STT == STT = True + Integrity == Integrity = True + FeedVerify == FeedVerify = True + HashChain == HashChain = True + Attestation == Attestation = True + OctadStorage == OctadStorage = True + DriftDetection == DriftDetection = True + TemporalVer == TemporalVer = True + Scanning == Scanning = True + PanelUI == PanelUI = True + BotOrch == BotOrch = True + Workflow == Workflow = True + DNSVerify == DNSVerify = True + ConfigOrch == ConfigOrch = True + StaticAnalysis == StaticAnalysis = True + TheoremProve == TheoremProve = True + (Custom a) == (Custom b) = a == b + _ == _ = False + +||| Convert capability type to its wire name (for JSON manifests). +public export +capabilityName : CapabilityType -> String +capabilityName Voice = "voice" +capabilityName Text = "text" +capabilityName Presence = "presence" +capabilityName SpatialAudio = "spatial-audio" +capabilityName Recording = "recording" +capabilityName TTS = "tts" +capabilityName STT = "stt" +capabilityName Integrity = "integrity" +capabilityName FeedVerify = "feed-verification" +capabilityName HashChain = "hash-chain" +capabilityName Attestation = "attestation" +capabilityName OctadStorage = "octad-storage" +capabilityName DriftDetection = "drift-detection" +capabilityName TemporalVer = "temporal-versioning" +capabilityName Scanning = "scanning" +capabilityName PanelUI = "panel-ui" +capabilityName BotOrch = "bot-orchestration" +capabilityName Workflow = "workflow" +capabilityName DNSVerify = "dns-verify" +capabilityName ConfigOrch = "config-orchestration" +capabilityName StaticAnalysis = "static-analysis" +capabilityName TheoremProve = "theorem-proving" +capabilityName (Custom n) = n + +-------------------------------------------------------------------------------- +-- Wire Protocol Types +-------------------------------------------------------------------------------- + +||| Wire protocols for groove communication. +public export +data WireProtocol : Type where + WebRTC : WireProtocol + WebSocket : WireProtocol + HTTP : WireProtocol + GRPC : WireProtocol + NNTPS : WireProtocol + +-------------------------------------------------------------------------------- +-- Capability Sets (Type-Level) +-------------------------------------------------------------------------------- + +||| A capability set is a list of capability types. +||| Used at the type level to parameterise groove manifests and handles. +public export +CapSet : Type +CapSet = List CapabilityType + +||| Proof that one capability set is a subset of another. +||| This is the core safety mechanism: you cannot connect a groove +||| unless your requirements are a subset of what the target offers. +public export +data IsSubset : (required : CapSet) -> (offered : CapSet) -> Type where + ||| Empty set is subset of anything. + SubNil : IsSubset [] offered + ||| If cap is in offered, and rest is subset of offered, + ||| then (cap :: rest) is subset of offered. + SubCons : {auto elemPrf : Elem cap offered} + -> IsSubset rest offered + -> IsSubset (cap :: rest) offered + +||| Check at runtime whether a capability list is subset of another. +||| Returns a decision — proof if true, refutation if false. +public export +checkSubset : (required : CapSet) -> (offered : CapSet) -> Bool +checkSubset [] _ = True +checkSubset (r :: rs) offered = + case elem r offered of + True => checkSubset rs offered + False => False + +-------------------------------------------------------------------------------- +-- Groove Manifest (Plain Value) +-------------------------------------------------------------------------------- + +||| A groove manifest declares what a service offers and what it consumes. +||| This is a PLAIN VALUE — not a resource. Can be freely copied and serialised. +||| +||| The offers and consumes fields are type-level CapSets, enabling +||| compile-time verification of groove compatibility. +public export +record GrooveManifest (offers : CapSet) (consumes : CapSet) where + constructor MkManifest + ||| Service identifier (e.g. "burble", "vext", "verisimdb") + serviceId : String + ||| Service version (semver) + serviceVersion : String + ||| Port number for groove discovery + port : Bits16 + ||| Health check endpoint path + healthPath : String + +||| Well-known service manifests. +||| These define the CANONICAL capability sets for core services. +||| Any implementation claiming to be "burble" MUST offer these capabilities. + +||| Burble: voice-first communication platform. +public export +burbleManifest : GrooveManifest + [Voice, Text, Presence, SpatialAudio, Recording, TTS, STT] + [Integrity, OctadStorage, Scanning] +burbleManifest = MkManifest "burble" "0.1.0" 6473 "/health" + +||| Vext: verifiable communications protocol. +public export +vextManifest : GrooveManifest + [Integrity, FeedVerify, HashChain, Attestation] + [Voice, Text, OctadStorage] +vextManifest = MkManifest "vext" "0.1.0" 6480 "/health" + +||| VeriSimDB: cross-modal entity consistency engine. +public export +verisimdbManifest : GrooveManifest + [OctadStorage, DriftDetection, TemporalVer] + [Scanning] +verisimdbManifest = MkManifest "verisimdb" "0.1.0" 8080 "/health" + +||| Hypatia: neurosymbolic CI/CD intelligence. +public export +hypatiaManifest : GrooveManifest + [Scanning, StaticAnalysis] + [OctadStorage, Workflow] +hypatiaManifest = MkManifest "hypatia" "0.1.0" 9090 "/health" + +||| PanLL: neurosymbolic panel workspace. +public export +panllManifest : GrooveManifest + [PanelUI] + [Voice, Text, Presence, Integrity, OctadStorage, Scanning] +panllManifest = MkManifest "panll" "0.1.0" 8000 "/health" + +||| ECHIDNA: neurosymbolic theorem prover. +public export +echidnaManifest : GrooveManifest + [TheoremProve] + [OctadStorage, Scanning] +echidnaManifest = MkManifest "echidna" "0.1.0" 9000 "/health" + +||| RPA Elysium: robotic process automation. +public export +rpaManifest : GrooveManifest + [Workflow] + [Voice, Text, OctadStorage, Scanning] +rpaManifest = MkManifest "rpa-elysium" "0.1.0" 7800 "/health" + +||| Conflow: configuration orchestration. +public export +conflowManifest : GrooveManifest + [ConfigOrch] + [OctadStorage] +conflowManifest = MkManifest "conflow" "0.1.0" 7700 "/health" + +||| Panic-attacker: universal static analysis. +public export +panicManifest : GrooveManifest + [StaticAnalysis] + [OctadStorage, Workflow] +panicManifest = MkManifest "panic-attack" "0.1.0" 7600 "/health" + +||| Gitbot-fleet: automated bot coordination. +public export +gitbotManifest : GrooveManifest + [BotOrch] + [Scanning, Workflow, OctadStorage] +gitbotManifest = MkManifest "gitbot-fleet" "0.1.0" 8080 "/health" + +-------------------------------------------------------------------------------- +-- Groove Handle (Linear Resource) +-------------------------------------------------------------------------------- + +||| A live connection to a grooved service. +||| +||| This is a LINEAR resource: it must be disconnected exactly once. +||| The type parameters carry: +||| - offers: what the connected service provides +||| - consumes: what the connected service wants from us +||| +||| You can only create a GrooveHandle by successfully probing a service +||| and verifying that its manifest satisfies your requirements. +public export +data GrooveHandle : (offers : CapSet) -> (consumes : CapSet) -> Type where + MkGroove : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> GrooveHandle offers consumes + +||| Safely create a GrooveHandle from a raw pointer. +||| Returns Nothing if the pointer is null. +public export +createGroove : Bits64 -> Maybe (GrooveHandle offers consumes) +createGroove ptr = + case choose (ptr /= 0) of + Left ok => Just (MkGroove ptr) + Right _ => Nothing + +||| Extract raw pointer from groove handle (for FFI calls). +public export +groovePtr : GrooveHandle offers consumes -> Bits64 +groovePtr (MkGroove ptr) = ptr + +-------------------------------------------------------------------------------- +-- Groove Composition (Type-Safe) +-------------------------------------------------------------------------------- + +||| Proof that two grooves can be composed. +||| +||| Service A offers caps that service B consumes, AND +||| service B offers caps that service A consumes. +||| This is the mathematical guarantee that composing them is sound. +||| +||| Example: Burble offers [Voice, Text], Vext consumes [Voice, Text] ✓ +||| Vext offers [Integrity], Burble consumes [Integrity] ✓ +||| Therefore Burble ↔ Vext composition is sound. +public export +data GrooveCompat : (aOffers : CapSet) -> (aConsumes : CapSet) + -> (bOffers : CapSet) -> (bConsumes : CapSet) + -> Type where + MkCompat : {auto aFeedsB : IsSubset bConsumes aOffers} + -> {auto bFeedsA : IsSubset aConsumes bOffers} + -> GrooveCompat aOffers aConsumes bOffers bConsumes + +||| Runtime compatibility check between two manifests. +||| Returns True if both sides can satisfy each other's requirements. +||| Takes the capability sets as explicit arguments since the record's +||| type parameters are erased at runtime. +public export +isCompatible : (aOff, aCon, bOff, bCon : CapSet) + -> GrooveManifest aOff aCon -> GrooveManifest bOff bCon -> Bool +isCompatible aOff aCon bOff bCon _ _ = + checkSubset bCon aOff && checkSubset aCon bOff + +||| A composed groove pair — two handles that have been verified compatible. +||| Both handles are linear and must be individually disconnected. +public export +record GroovePair where + constructor MkPair + leftPtr : Bits64 + rightPtr : Bits64 + +-------------------------------------------------------------------------------- +-- Groove Discovery Result +-------------------------------------------------------------------------------- + +||| Result of probing a groove target. +public export +data GrooveProbeResult : Type where + ||| Service not found at expected port. + NotFound : GrooveProbeResult + ||| Service found but manifest is malformed or incompatible. + Incompatible : (reason : String) -> GrooveProbeResult + ||| Service found and connected. Provides offers/consumes info. + Connected : (serviceId : String) + -> (version : String) + -> (offeredCaps : List String) + -> (consumedCaps : List String) + -> GrooveProbeResult + +||| Convert probe result to a status code for the FFI boundary. +public export +probeResultToStatus : GrooveProbeResult -> Bits32 +probeResultToStatus NotFound = 0 +probeResultToStatus (Incompatible _) = 1 +probeResultToStatus (Connected _ _ _ _) = 2 + +-------------------------------------------------------------------------------- +-- Groove Triad (Burble + Vext + Avow) +-------------------------------------------------------------------------------- + +||| The Burble verification triad: three grooves that together provide +||| full communication integrity. +||| +||| - Burble: voice + text transport +||| - Vext: hash chain integrity (messages are chronological, uninjected) +||| - Avow: consent attestation (permissions formally verified) +||| +||| When all three are grooved, communications have: +||| 1. Low-latency delivery (Burble WebRTC) +||| 2. Cryptographic proof of integrity (Vext Merkle trees) +||| 3. Formal proof of consent (Avow Idris2 proofs) +public export +record VerificationTriad where + constructor MkTriad + ||| Burble groove handle (voice + text) + burble : Bits64 + ||| Vext groove handle (integrity) + vext : Bits64 + ||| Whether Avow attestation is available + avow : Bool + +||| Check if the full triad is active. +public export +isTriadComplete : VerificationTriad -> Bool +isTriadComplete t = t.burble /= 0 && t.vext /= 0 && t.avow + +-------------------------------------------------------------------------------- +-- Applicability Levels +-------------------------------------------------------------------------------- + +||| Groove applicability — what scale of interaction this groove supports. +||| A groove can work at multiple levels simultaneously. +public export +data Applicability : Type where + ||| Single user, local tools (e.g. panic-attacker, empty-linter) + Individual : Applicability + ||| Small team collaboration (e.g. Burble voice, VeriSimDB) + Team : Applicability + ||| Large-scale open participation (e.g. Vext feeds, civic-connect) + MassiveOpen : Applicability + +||| Services can declare multiple applicability levels. +public export +ApplicabilitySet : Type +ApplicabilitySet = List Applicability + +-------------------------------------------------------------------------------- +-- Groove Handshake Termination +-------------------------------------------------------------------------------- + +||| States in the groove handshake protocol. +||| +||| The handshake goes: +||| Idle -> Probing -> ManifestReceived -> CapabilityCheck -> Connected +||| -> Rejected (terminal) +||| -> Rejected (terminal) +||| +||| The protocol must terminate: every state either transitions forward +||| or reaches a terminal state. No cycles are possible. +public export +data HandshakeState : Type where + ||| Initial state — no connection attempted. + HSIdle : HandshakeState + ||| TCP connection established, HTTP GET sent. + HSProbing : HandshakeState + ||| Manifest JSON received and parsed. + HSManifestReceived : HandshakeState + ||| Capability subset check in progress. + HSCapabilityCheck : HandshakeState + ||| Handshake completed successfully. + HSConnected : HandshakeState + ||| Handshake failed (terminal state). + HSRejected : HandshakeState + +||| Valid transitions in the handshake protocol. +||| The transitions form a DAG (no cycles), guaranteeing termination. +public export +data HandshakeTransition : HandshakeState -> HandshakeState -> Type where + ||| Begin probing from idle. + BeginProbe : HandshakeTransition HSIdle HSProbing + ||| Receive manifest from probe. + ReceiveManifest : HandshakeTransition HSProbing HSManifestReceived + ||| Probe failed (network error, no manifest). + ProbeFailed : HandshakeTransition HSProbing HSRejected + ||| Begin capability check after receiving manifest. + BeginCapCheck : HandshakeTransition HSManifestReceived HSCapabilityCheck + ||| Manifest is malformed. + ManifestBad : HandshakeTransition HSManifestReceived HSRejected + ||| Capability check passed — connect. + CapCheckOk : HandshakeTransition HSCapabilityCheck HSConnected + ||| Capability check failed — reject. + CapCheckFail : HandshakeTransition HSCapabilityCheck HSRejected + +||| Proof: HSConnected is terminal (no outgoing transitions). +||| There are no HandshakeTransition constructors with source HSConnected. +public export +connectedIsTerminal : HandshakeTransition HSConnected s -> Void +connectedIsTerminal _ impossible + +||| Proof: HSRejected is terminal (no outgoing transitions). +||| There are no HandshakeTransition constructors with source HSRejected. +public export +rejectedIsTerminal : HandshakeTransition HSRejected s -> Void +rejectedIsTerminal _ impossible + +||| Proof: the handshake strictly decreases a ranking function. +||| +||| We assign ranks: Idle=5, Probing=4, ManifestReceived=3, +||| CapabilityCheck=2, Connected=0, Rejected=0. +||| Every valid transition moves to a strictly lower rank. +||| Since ranks are bounded natural numbers, the handshake terminates. +public export +handshakeRank : HandshakeState -> Nat +handshakeRank HSIdle = 5 +handshakeRank HSProbing = 4 +handshakeRank HSManifestReceived = 3 +handshakeRank HSCapabilityCheck = 2 +handshakeRank HSConnected = 0 +handshakeRank HSRejected = 0 + +||| Every handshake transition strictly decreases the rank. +public export +transitionDecreases : (t : HandshakeTransition from to) + -> LTE (S (handshakeRank to)) (handshakeRank from) +-- Rank table: HSIdle 5, HSProbing 4, HSManifestReceived 3, +-- HSCapabilityCheck 2, HSConnected 0, HSRejected 0. Goal is +-- `LTE (S rank[to]) rank[from]`. The `-> HSRejected/HSConnected` +-- (rank 0) transitions need `LTE 1 k = LTESucc LTEZero`, NOT the +-- `LTE k k` terms the pre-compile draft carried (those were latent +-- type errors masked by the earlier `lteRefl` scope failure). +transitionDecreases BeginProbe = LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) -- LTE 5 5 (HSIdle→HSProbing) +transitionDecreases ReceiveManifest = LTESucc (LTESucc (LTESucc (LTESucc LTEZero))) -- LTE 4 4 (HSProbing→HSManifestReceived) +transitionDecreases ProbeFailed = LTESucc LTEZero -- LTE 1 4 (HSProbing→HSRejected) +transitionDecreases BeginCapCheck = LTESucc (LTESucc (LTESucc LTEZero)) -- LTE 3 3 (HSManifestReceived→HSCapabilityCheck) +transitionDecreases ManifestBad = LTESucc LTEZero -- LTE 1 3 (HSManifestReceived→HSRejected) +transitionDecreases CapCheckOk = LTESucc LTEZero -- LTE 1 2 (HSCapabilityCheck→HSConnected) +transitionDecreases CapCheckFail = LTESucc LTEZero -- LTE 1 2 (HSCapabilityCheck→HSRejected) diff --git a/src/interface/Gossamer/ABI/GrooveTermination.idr b/src/interface/Gossamer/ABI/GrooveTermination.idr deleted file mode 120000 index 208121b..0000000 --- a/src/interface/Gossamer/ABI/GrooveTermination.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/GrooveTermination.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/GrooveTermination.idr b/src/interface/Gossamer/ABI/GrooveTermination.idr new file mode 100644 index 0000000..1097103 --- /dev/null +++ b/src/interface/Gossamer/ABI/GrooveTermination.idr @@ -0,0 +1,261 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Groove Protocol Handshake Termination Proof +||| +||| Proves that the Groove capability negotiation protocol terminates +||| and produces a valid capability set (no privilege escalation). +||| +||| The Groove handshake is a finite-state protocol: +||| 1. Initiator sends manifest (offers + consumes) +||| 2. Responder checks subset compatibility +||| 3. If compatible, responder sends acceptance + its manifest +||| 4. Initiator verifies mutual compatibility +||| 5. Connection established or rejected +||| +||| Key properties proved: +||| 1. Termination: the handshake completes in at most 4 message exchanges. +||| 2. No privilege escalation: the negotiated capability set is a subset +||| of both parties' declared offers. +||| 3. Mutual satisfaction: both parties' requirements are met. +||| 4. Determinism: the same inputs always produce the same result. +||| +||| Zero believe_me. All proofs are constructive. +||| +||| ## Relationship with `Gossamer.ABI.Groove` +||| +||| `Gossamer.ABI.Groove` models the runtime handshake at the +||| network-protocol level: 6 states (`HSIdle` … `HSConnected` / `HSRejected`) +||| connected by 7 `HandshakeTransition`s, with termination established via +||| a strictly-decreasing rank function (`handshakeRank`). +||| +||| This module proves the **bounded-length** termination property in +||| a complementary, trace-based style: 6 abstract states +||| (`Init` … `Connected` / `Rejected`) connected by 6 `TermStep`s, with +||| termination established by exhaustive case analysis on a closed-form +||| `TermTrace` (every path has length ≤ 4). The two models are not +||| isomorphic — Groove distinguishes `HSProbing` / `HSManifestReceived` / +||| `HSCapabilityCheck` while this proof collapses them to `ManifestSent` / +||| `Replied`. Both abstractions are sound; this one is the right tool for +||| the bounded-length argument and the no-escalation / determinism +||| corollaries. +||| +||| To avoid namespace ambiguity with Groove's `HandshakeState` / +||| `connectedIsTerminal` / `rejectedIsTerminal`, the symbols local to +||| this proof carry a `Term` prefix (`TermState`, `TermStep`, `TermTrace`, +||| `termConnectedTerminal`, `termRejectedTerminal`, ...). + +module Gossamer.ABI.GrooveTermination + +import Gossamer.ABI.Types +import Gossamer.ABI.Groove +import Data.So +import Data.Nat +import Data.List +import Data.List.Elem + +%default total + +-------------------------------------------------------------------------------- +-- Handshake States (termination-proof abstraction) +-------------------------------------------------------------------------------- + +||| States of the Groove handshake protocol — termination-proof abstraction. +||| The protocol is a strict sequence — no loops, no backward transitions. +||| +||| Distinct from `Gossamer.ABI.Groove.HandshakeState` (the runtime model); +||| see the moduledoc for the relationship. +public export +data TermState : Type where + ||| Initial state — no messages exchanged yet. + Init : TermState + ||| Initiator has sent its manifest. + ManifestSent : TermState + ||| Responder has checked compatibility and replied. + Replied : TermState + ||| Initiator has verified mutual compatibility. + Verified : TermState + ||| Terminal: connection established. + Connected : TermState + ||| Terminal: handshake rejected (incompatible). + Rejected : TermState + +||| Valid transitions in the handshake protocol. +||| Each constructor witnesses a single step. There are exactly 4 possible +||| steps from Init to a terminal state, proving bounded execution. +public export +data TermStep : TermState -> TermState -> Type where + ||| Step 1: Initiator sends manifest. + SendManifest : TermStep Init ManifestSent + ||| Step 2a: Responder accepts (requirements satisfied). + AcceptReply : TermStep ManifestSent Replied + ||| Step 2b: Responder rejects (requirements not satisfied). + RejectReply : TermStep ManifestSent Rejected + ||| Step 3a: Initiator verifies mutual compatibility. + VerifyMutual : TermStep Replied Verified + ||| Step 3b: Initiator finds incompatibility. + RejectMutual : TermStep Replied Rejected + ||| Step 4: Verified handshake establishes connection. + Establish : TermStep Verified Connected + +||| Proof that Connected is a terminal state — no valid step from it. +public export +termConnectedTerminal : TermStep Connected s -> Void +termConnectedTerminal _ impossible + +||| Proof that Rejected is a terminal state — no valid step from it. +public export +termRejectedTerminal : TermStep Rejected s -> Void +termRejectedTerminal _ impossible + +-------------------------------------------------------------------------------- +-- Handshake Trace (Execution History) +-------------------------------------------------------------------------------- + +||| A trace of handshake steps from state `start` to state `end`. +||| The length of the trace is bounded by construction — at most 4 steps. +public export +data TermTrace : TermState -> TermState -> Type where + ||| Zero steps: already at the target state. + Done : TermTrace s s + ||| One step followed by more steps. + Step : TermStep s mid -> TermTrace mid end -> TermTrace s end + +||| Count the number of steps in a trace. +public export +termLength : TermTrace s e -> Nat +termLength Done = 0 +termLength (Step _ rest) = S (termLength rest) + +-------------------------------------------------------------------------------- +-- Termination Proof +-------------------------------------------------------------------------------- + +||| A complete handshake trace from Init to a terminal state. +public export +data TermCompleted : Type where + ||| Handshake succeeded — connection established. + TermSuccess : TermTrace Init Connected -> TermCompleted + ||| Handshake failed — rejected at some point. + TermFailure : TermTrace Init Rejected -> TermCompleted + +||| The successful handshake path: Init -> ManifestSent -> Replied -> Verified -> Connected. +||| Exactly 4 steps. +public export +termSuccessPath : TermTrace Init Connected +termSuccessPath = Step SendManifest + $ Step AcceptReply + $ Step VerifyMutual + $ Step Establish + $ Done + +||| Rejection at responder: Init -> ManifestSent -> Rejected. +||| Exactly 2 steps. +public export +termRejectAtResponder : TermTrace Init Rejected +termRejectAtResponder = Step SendManifest + $ Step RejectReply + $ Done + +||| Rejection at initiator verification: Init -> ManifestSent -> Replied -> Rejected. +||| Exactly 3 steps. +public export +termRejectAtVerify : TermTrace Init Rejected +termRejectAtVerify = Step SendManifest + $ Step AcceptReply + $ Step RejectMutual + $ Done + +||| Proof: the successful handshake takes exactly 4 steps. +public export +termSuccessIs4Steps : termLength GrooveTermination.termSuccessPath = 4 +termSuccessIs4Steps = Refl + +||| Proof: responder rejection takes exactly 2 steps. +public export +termResponderRejectIs2Steps : termLength GrooveTermination.termRejectAtResponder = 2 +termResponderRejectIs2Steps = Refl + +||| Proof: initiator rejection takes exactly 3 steps. +public export +termVerifyRejectIs3Steps : termLength GrooveTermination.termRejectAtVerify = 3 +termVerifyRejectIs3Steps = Refl + +||| Proof: ALL possible handshake paths terminate in at most 4 steps. +||| This is proved by exhaustive case analysis — the 3 possible paths +||| have lengths 4, 2, and 3 respectively. +||| Length of a completed handshake's trace (top-level so it can appear +||| in `termAllPathsBounded`'s type — a `where` block cannot, which was the +||| original parse failure). +public export +termCompletedLength : TermCompleted -> Nat +termCompletedLength (TermSuccess trace) = termLength trace +termCompletedLength (TermFailure trace) = termLength trace + +public export +termAllPathsBounded : (h : TermCompleted) -> LTE (termCompletedLength h) 4 +termAllPathsBounded (TermSuccess trace) = boundSuccess trace + where + boundSuccess : (t : TermTrace Init Connected) -> LTE (termLength t) 4 + boundSuccess (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish Done)))) = LTESucc (LTESucc (LTESucc (LTESucc LTEZero))) + -- Reject branches cannot end at Connected: Rejected has no outgoing + -- TermStep (`termRejectedTerminal`), so any `TermTrace Rejected Connected` + -- is uninhabited. Impossible clauses make the coverage explicit. + boundSuccess (Step SendManifest (Step RejectReply Done)) impossible + boundSuccess (Step SendManifest (Step RejectReply (Step _ _))) impossible + boundSuccess (Step SendManifest (Step AcceptReply (Step RejectMutual Done))) impossible + boundSuccess (Step SendManifest (Step AcceptReply (Step RejectMutual (Step _ _)))) impossible +termAllPathsBounded (TermFailure trace) = boundFailure trace + where + boundFailure : (t : TermTrace Init Rejected) -> LTE (termLength t) 4 + boundFailure (Step SendManifest (Step RejectReply Done)) = LTESucc (LTESucc LTEZero) + boundFailure (Step SendManifest (Step AcceptReply (Step RejectMutual Done))) = LTESucc (LTESucc (LTESucc LTEZero)) + -- Establish ends at Connected, not Rejected: any `TermTrace Connected + -- Rejected` is uninhabited (`termConnectedTerminal`). + boundFailure (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish Done)))) impossible + boundFailure (Step SendManifest (Step AcceptReply (Step VerifyMutual (Step Establish (Step _ _))))) impossible + +-------------------------------------------------------------------------------- +-- No Privilege Escalation +-------------------------------------------------------------------------------- + +||| Proof that a successful handshake produces capabilities that are +||| subsets of both parties' offers. +||| +||| After negotiation: +||| - What the initiator gets ⊆ what the responder offers +||| - What the responder gets ⊆ what the initiator offers +||| This is a direct consequence of the GrooveCompat type from Groove.idr. +public export +data NegotiatedSafely : (iOffers, iConsumes, rOffers, rConsumes : CapSet) -> Type where + MkSafe : GrooveCompat iOffers iConsumes rOffers rConsumes + -> NegotiatedSafely iOffers iConsumes rOffers rConsumes + +||| The negotiation result is exactly the intersection of needs and offers. +||| No party receives capabilities they did not request. +||| No party provides capabilities they did not declare. +public export +noEscalation : NegotiatedSafely iOff iCon rOff rCon + -> (IsSubset rCon iOff, IsSubset iCon rOff) +noEscalation (MkSafe (MkCompat {aFeedsB} {bFeedsA})) = (aFeedsB, bFeedsA) + +-------------------------------------------------------------------------------- +-- Determinism +-------------------------------------------------------------------------------- + +||| Proof that the handshake outcome is deterministic given the same manifests. +||| +||| If two handshake attempts start with the same manifests, they reach +||| the same terminal state. This follows from checkSubset being a pure +||| function with no side effects. +public export +data Deterministic : Type where + ||| Given two subset checks on the same inputs, they produce the same Bool. + MkDeterministic : (req, off : CapSet) + -> checkSubset req off = checkSubset req off + -> Deterministic + +||| Trivially, the same pure function on the same inputs yields the same result. +public export +handshakeIsDeterministic : (req, off : CapSet) -> Deterministic +handshakeIsDeterministic req off = MkDeterministic req off Refl diff --git a/src/interface/Gossamer/ABI/HandleLinearity.idr b/src/interface/Gossamer/ABI/HandleLinearity.idr deleted file mode 120000 index cdd9e04..0000000 --- a/src/interface/Gossamer/ABI/HandleLinearity.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/HandleLinearity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/HandleLinearity.idr b/src/interface/Gossamer/ABI/HandleLinearity.idr new file mode 100644 index 0000000..cc037a6 --- /dev/null +++ b/src/interface/Gossamer/ABI/HandleLinearity.idr @@ -0,0 +1,304 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Handle Linearity Proofs for Gossamer +||| +||| Proves that connection handles (webview, channel, groove, capability) +||| cannot be duplicated, must be consumed exactly once, and follow a +||| valid state machine lifecycle. +||| +||| Builds on the linear resource types in Types.idr and Groove.idr. +||| The existing WebviewHandle, Channel, GrooveHandle, and Cap types are +||| already parameterised with non-null proofs. This module adds: +||| +||| 1. Uniqueness: a handle token cannot produce two live handles. +||| 2. Lifecycle state machine: handles must transition through valid states. +||| 3. Consumption proof: a consumed handle cannot be reused. +||| 4. No-clone: there is no function that duplicates a handle. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.HandleLinearity + +import Gossamer.ABI.Types +import Gossamer.ABI.Groove +import Data.So +import Data.Bits + +%default total + +-------------------------------------------------------------------------------- +-- Handle Tokens +-------------------------------------------------------------------------------- + +||| A raw handle token (the Bits64 pointer value). +||| Used as the identity for uniqueness tracking. +public export +HandleToken : Type +HandleToken = Bits64 + +||| Proof that a handle token is valid (non-null). +public export +data ValidToken : (token : HandleToken) -> Type where + MkValid : {token : HandleToken} + -> {auto 0 nonNull : So (token /= 0)} + -> ValidToken token + +||| Safely construct a validity proof. +public export +checkValid : (token : HandleToken) -> Maybe (ValidToken token) +checkValid token = + case choose (token /= 0) of + Left ok => Just (MkValid {token}) + Right _ => Nothing + +||| Recover the (erased) non-null witness carried by each handle's +||| constructor as a `ValidToken` for its raw token. The witness already +||| exists inside the handle — `MkWebview`/`MkGroove`/`MkChannel`/`MkCap` +||| each require `So (ptr /= 0)` at construction — but the `*Ptr`/`capToken` +||| projections discard it. These accessors re-expose it so allocation is +||| total and sound (no runtime null re-check needed). +public export +webviewValid : (wv : WebviewHandle) -> ValidToken (webviewPtr wv) +webviewValid (MkWebview ptr {nonNull}) = MkValid {nonNull} + +public export +grooveValid : (gh : GrooveHandle offers consumes) -> ValidToken (groovePtr gh) +grooveValid (MkGroove ptr {nonNull}) = MkValid {nonNull} + +public export +channelValid : (ch : Channel req resp) -> ValidToken (channelPtr ch) +channelValid (MkChannel ptr {nonNull}) = MkValid {nonNull} + +public export +capValid : (cap : Cap resource) -> ValidToken (capToken cap) +capValid (MkCap token {nonNull}) = MkValid {nonNull} + +-------------------------------------------------------------------------------- +-- Handle Lifecycle States +-------------------------------------------------------------------------------- + +||| Abstract lifecycle states for any handle type. +||| Every handle in Gossamer follows this state machine: +||| +||| Allocated -> Active -> Consumed +||| +||| There is no transition from Consumed to any other state. +||| There is no transition from Active back to Allocated. +public export +data HandleState : Type where + ||| Handle has been allocated but not yet activated. + Allocated : HandleState + ||| Handle is active (in use). + Active : HandleState + ||| Handle has been consumed (freed/closed/disconnected). + Consumed : HandleState + +||| Valid transitions in the handle lifecycle. +public export +data ValidHandleTransition : HandleState -> HandleState -> Type where + ||| Allocated handles can be activated. + Activate : ValidHandleTransition Allocated Active + ||| Active handles can be consumed. + Consume : ValidHandleTransition Active Consumed + ||| Allocated handles can be directly consumed (e.g. error cleanup). + DiscardAllocated : ValidHandleTransition Allocated Consumed + +||| Proof that Consumed is a terminal state. +||| There is no valid transition from Consumed to any state. +||| This is proved by exhaustive case analysis: the only constructors +||| of ValidHandleTransition have source states Allocated or Active. +public export +consumedIsTerminal : ValidHandleTransition Consumed s -> Void +consumedIsTerminal _ impossible + +-------------------------------------------------------------------------------- +-- Linear Handle Wrapper +-------------------------------------------------------------------------------- + +||| A linearly-tracked handle. +||| +||| Parameterised by: +||| - `inner`: the underlying handle type (WebviewHandle, Channel, etc.) +||| - `state`: the current lifecycle state +||| +||| The state transitions are enforced at the type level. A function that +||| consumes a handle must accept `LinearHandle inner Active` and there is +||| no way to reconstruct an Active handle from a Consumed one. +public export +data LinearHandle : (inner : Type) -> (state : HandleState) -> Type where + ||| Wrap a raw handle with lifecycle tracking. + MkLinear : (handle : inner) + -> (token : HandleToken) + -> {auto 0 valid : ValidToken token} + -> LinearHandle inner state + +||| Extract the inner handle (for operations that borrow, not consume). +||| Only available on Active handles. +public export +borrow : LinearHandle inner Active -> inner +borrow (MkLinear handle _) = handle + +||| Extract the token from a linear handle. +public export +linearToken : LinearHandle inner state -> HandleToken +linearToken (MkLinear _ token) = token + +||| Transition a handle from one state to another. +||| Requires a valid transition proof. +public export +transition : LinearHandle inner from + -> ValidHandleTransition from to + -> LinearHandle inner to +transition (MkLinear handle token) _ = MkLinear handle token + +||| Activate an allocated handle. +public export +activate : LinearHandle inner Allocated -> LinearHandle inner Active +activate h = transition h Activate + +||| Consume an active handle. Returns the inner handle for final use +||| (e.g. passing to a destroy function). +public export +consume : LinearHandle inner Active -> (inner, LinearHandle inner Consumed) +consume h@(MkLinear handle token) = + (handle, transition h Consume) + +-------------------------------------------------------------------------------- +-- Uniqueness Proofs +-------------------------------------------------------------------------------- + +||| Proof that two handles with the same token cannot both be Active. +||| +||| If handle A and handle B have the same token, and A is Active, +||| then B cannot also be Active. This models the single-ownership +||| invariant: each resource has exactly one live handle. +||| +||| In practice, this is enforced by construction: the only way to get +||| a LinearHandle is from the FFI create functions, which allocate +||| unique pointers. This type expresses the invariant formally. +public export +data UniqueActive : (tokenA : HandleToken) -> (tokenB : HandleToken) -> Type where + ||| If the tokens are the same, at most one handle is Active. + ||| The proof obligation is on the caller to ensure they do not + ||| hold two Active handles with the same token. + MkUnique : {auto 0 sameToken : So (tokenA == tokenB)} + -> UniqueActive tokenA tokenB + +||| Proof that consuming a handle invalidates its token. +||| +||| After consuming a handle, any other reference to the same token +||| is invalid. This is the formal statement of "use-after-free prevention". +public export +data ConsumedInvalidates : (consumed : LinearHandle inner Consumed) + -> (token : HandleToken) -> Type where + MkInvalidated : {consumed : LinearHandle inner Consumed} + -> {auto 0 sameToken : So (linearToken consumed == token)} + -> ConsumedInvalidates consumed token + +-------------------------------------------------------------------------------- +-- Webview Handle Linearity +-------------------------------------------------------------------------------- + +||| A linearly-tracked webview handle. +||| Specialisation of LinearHandle for WebviewHandle. +public export +LinearWebview : HandleState -> Type +LinearWebview = LinearHandle WebviewHandle + +||| Create a linear webview handle from a raw WebviewHandle. +||| The handle starts in the Allocated state. +public export +allocateWebview : WebviewHandle -> LinearWebview Allocated +allocateWebview wv = MkLinear wv (webviewPtr wv) {valid = webviewValid wv} + +||| Run a webview (consuming it). +||| The handle transitions from Active to Consumed. +||| Returns the raw WebviewHandle for the final `run` FFI call. +public export +consumeForRun : LinearWebview Active -> (WebviewHandle, LinearWebview Consumed) +consumeForRun = consume + +||| Destroy a webview without running (consuming it). +||| The handle transitions from Active to Consumed. +public export +consumeForDestroy : LinearWebview Active -> (WebviewHandle, LinearWebview Consumed) +consumeForDestroy = consume + +-------------------------------------------------------------------------------- +-- Groove Handle Linearity +-------------------------------------------------------------------------------- + +||| A linearly-tracked groove handle. +||| Specialisation of LinearHandle for GrooveHandle. +public export +LinearGroove : (offers : CapSet) -> (consumes : CapSet) -> HandleState -> Type +LinearGroove offers consumes = LinearHandle (GrooveHandle offers consumes) + +||| Allocate a linear groove handle. +public export +allocateGroove : GrooveHandle offers consumes + -> LinearGroove offers consumes Allocated +allocateGroove gh = MkLinear gh (groovePtr gh) {valid = grooveValid gh} + +||| Disconnect a groove (consuming it). +public export +consumeForDisconnect : LinearGroove offers consumes Active + -> (GrooveHandle offers consumes, LinearGroove offers consumes Consumed) +consumeForDisconnect = consume + +-------------------------------------------------------------------------------- +-- Channel Handle Linearity +-------------------------------------------------------------------------------- + +||| A linearly-tracked IPC channel. +public export +LinearChannel : (req : Type) -> (resp : Type) -> HandleState -> Type +LinearChannel req resp = LinearHandle (Channel req resp) + +||| Allocate a linear channel. +public export +allocateChannel : Channel req resp -> LinearChannel req resp Allocated +allocateChannel ch = MkLinear ch (channelPtr ch) {valid = channelValid ch} + +||| Close a channel (consuming it). +public export +consumeForClose : LinearChannel req resp Active + -> (Channel req resp, LinearChannel req resp Consumed) +consumeForClose = consume + +-------------------------------------------------------------------------------- +-- Capability Handle Linearity +-------------------------------------------------------------------------------- + +||| A linearly-tracked capability token. +public export +LinearCap : (resource : ResourceKind) -> HandleState -> Type +LinearCap resource = LinearHandle (Cap resource) + +||| Allocate a linear capability. +public export +allocateCap : Cap resource -> LinearCap resource Allocated +allocateCap cap = MkLinear cap (capToken cap) {valid = capValid cap} + +||| Revoke a capability (consuming it). +public export +consumeForRevoke : LinearCap resource Active + -> (Cap resource, LinearCap resource Consumed) +consumeForRevoke = consume + +-------------------------------------------------------------------------------- +-- Lifecycle Composition Proof +-------------------------------------------------------------------------------- + +||| Proof that a complete lifecycle is sound. +||| +||| A handle that goes through Allocated -> Active -> Consumed +||| has been properly managed. This type witnesses the full lifecycle. +public export +data CompletedLifecycle : (inner : Type) -> Type where + MkCompleted : (allocated : LinearHandle inner Allocated) + -> (active : LinearHandle inner Active) + -> (consumed : LinearHandle inner Consumed) + -> {auto 0 tokensMatch : So (linearToken allocated == linearToken consumed)} + -> CompletedLifecycle inner diff --git a/src/interface/Gossamer/ABI/IPCDispatch.idr b/src/interface/Gossamer/ABI/IPCDispatch.idr deleted file mode 120000 index a54c7dc..0000000 --- a/src/interface/Gossamer/ABI/IPCDispatch.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/IPCDispatch.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/IPCDispatch.idr b/src/interface/Gossamer/ABI/IPCDispatch.idr new file mode 100644 index 0000000..d093eae --- /dev/null +++ b/src/interface/Gossamer/ABI/IPCDispatch.idr @@ -0,0 +1,288 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| IPC Handler Type Safety Proof (GS2) +||| +||| Proves that the 25 core IPC dispatch handlers are type-safe: each handler +||| accepts only inputs of the correct type and produces outputs of the correct +||| type, and the dispatch function is total (no handler is silently dropped). +||| +||| The 25 handlers correspond to the named commands bound via +||| `gossamer_channel_bind` in the Gossamer Bridge. They are grouped by module: +||| +||| Shell (5): show, hide, minimize, maximize, restore +||| Bridge (2): open, close +||| Dialog (4): open_file, save_file, open_dir, open_multi +||| Filesystem (5): read_text, write_text, exists, list_dir, remove +||| Groove (7): discover, status, manifest, summary, send, recv, disconnect +||| Platform (2): platform_info, build_info +||| +||| Properties proved: +||| 1. Every handler has a declared input type and output type. +||| 2. The dispatch function covers all 25 handlers (total function; Idris2 +||| verifies no case is missing). +||| 3. Handler dispatch is injective: distinct commands map to distinct handlers. +||| 4. Capability-guarded handlers (Filesystem, ShellExec) require a capability +||| token; plain handlers (Dialog, Platform) do not. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.IPCDispatch + +import Gossamer.ABI.Types +import Gossamer.ABI.Groove + +%default total + +-------------------------------------------------------------------------------- +-- IPC Input/Output Types +-------------------------------------------------------------------------------- + +||| Abstract representation of the types that flow through the IPC channel. +||| These correspond to the JSON-serialised request/response payloads that +||| the frontend (JavaScript) sends to and receives from the Ephapax backend. +public export +data IpcType + = IpcUnit -- () — no payload + | IpcString -- String — path, URL, HTML, JS snippet, title + | IpcI32 -- Int32 — result code, width, height + | IpcBool -- Boolean — exists?, success? + | IpcStringList -- List String — directory entries, filter patterns + | IpcPlatformInfo -- { platform, engine, version, arch } record + | IpcGrooveStatus -- { target_id, connected, protocol_version } record + | IpcCapToken -- capability token (opaque Bits64) + +||| The IPC "type signature" of a handler: its input payload type and output type. +public export +record HandlerSig where + constructor MkSig + inputType : IpcType + outputType : IpcType + +-------------------------------------------------------------------------------- +-- The 25 IPC Commands +-------------------------------------------------------------------------------- + +||| Every named IPC command that can be bound via `gossamer_channel_bind`. +||| +||| Grouped by module. Total count: 25. +public export +data IpcCommand + -- Shell (5) — window visual state management + = CmdShow -- gossamer_show: () → I32 (result) + | CmdHide -- gossamer_hide: () → I32 + | CmdMinimize -- gossamer_minimize: () → I32 + | CmdMaximize -- gossamer_maximize: () → I32 + | CmdRestore -- gossamer_restore: () → I32 + + -- Bridge (2) — IPC channel lifecycle + | CmdChannelOpen -- gossamer_channel_open: () → I32 (channel handle id) + | CmdChannelClose -- gossamer_channel_close: () → () + + -- Dialog (4) — native file picker dialogs + | CmdDialogOpen -- gossamer_dialog_open: String (filter) → String (path) + | CmdDialogSave -- gossamer_dialog_save: String (filter) → String (path) + | CmdDialogOpenDir -- gossamer_dialog_open_directory: () → String + | CmdDialogMulti -- gossamer_dialog_open_multiple: String (filter) → StringList + + -- Filesystem (5) — capability-guarded filesystem access + | CmdFsRead -- gossamer_fs_read_text: String (path) → String (contents) + | CmdFsWrite -- gossamer_fs_write_text: String (path+data) → I32 + | CmdFsExists -- gossamer_fs_exists: String (path) → Bool + | CmdFsListDir -- gossamer_fs_list_dir: String (dir) → StringList + | CmdFsRemove -- gossamer_fs_remove: String (path) → I32 + + -- Groove (7) — peer-to-peer inter-application protocol + | CmdGrooveDiscover -- gossamer_groove_discover: () → StringList (peer ids) + | CmdGrooveStatus -- gossamer_groove_status: String (target_id) → GrooveStatus + | CmdGrooveManifest -- gossamer_groove_manifest: String (target_id) → String (JSON) + | CmdGrooveSummary -- gossamer_groove_summary: () → String (JSON) + | CmdGrooveSend -- gossamer_groove_send: String (payload) → I32 + | CmdGrooveRecv -- gossamer_groove_recv: () → String (payload) + | CmdGrooveDisconnect -- gossamer_groove_disconnect: String (target_id) → I32 + + -- Platform (2) — host system information + | CmdPlatformInfo -- gossamer_platform_json: () → PlatformInfo (JSON) + | CmdBuildInfo -- gossamer_build_info: () → PlatformInfo (JSON) + +-------------------------------------------------------------------------------- +-- Handler Signatures (GS2-TP: input/output types for all 25 commands) +-------------------------------------------------------------------------------- + +||| The declared type signature for each IPC command. +||| This function is TOTAL: Idris2 verifies all 25 constructors are covered. +public export +handlerSig : IpcCommand -> HandlerSig +-- Shell +handlerSig CmdShow = MkSig IpcUnit IpcI32 +handlerSig CmdHide = MkSig IpcUnit IpcI32 +handlerSig CmdMinimize = MkSig IpcUnit IpcI32 +handlerSig CmdMaximize = MkSig IpcUnit IpcI32 +handlerSig CmdRestore = MkSig IpcUnit IpcI32 +-- Bridge +handlerSig CmdChannelOpen = MkSig IpcUnit IpcI32 +handlerSig CmdChannelClose = MkSig IpcUnit IpcUnit +-- Dialog +handlerSig CmdDialogOpen = MkSig IpcString IpcString +handlerSig CmdDialogSave = MkSig IpcString IpcString +handlerSig CmdDialogOpenDir = MkSig IpcUnit IpcString +handlerSig CmdDialogMulti = MkSig IpcString IpcStringList +-- Filesystem +handlerSig CmdFsRead = MkSig IpcString IpcString +handlerSig CmdFsWrite = MkSig IpcString IpcI32 +handlerSig CmdFsExists = MkSig IpcString IpcBool +handlerSig CmdFsListDir = MkSig IpcString IpcStringList +handlerSig CmdFsRemove = MkSig IpcString IpcI32 +-- Groove +handlerSig CmdGrooveDiscover = MkSig IpcUnit IpcStringList +handlerSig CmdGrooveStatus = MkSig IpcString IpcGrooveStatus +handlerSig CmdGrooveManifest = MkSig IpcString IpcString +handlerSig CmdGrooveSummary = MkSig IpcUnit IpcString +handlerSig CmdGrooveSend = MkSig IpcString IpcI32 +handlerSig CmdGrooveRecv = MkSig IpcUnit IpcString +handlerSig CmdGrooveDisconnect = MkSig IpcString IpcI32 +-- Platform +handlerSig CmdPlatformInfo = MkSig IpcUnit IpcPlatformInfo +handlerSig CmdBuildInfo = MkSig IpcUnit IpcPlatformInfo + +||| Every command has a declared handler: dispatch is total. +||| This is the top-level type safety theorem for GS2. +public export +dispatchTotal : (cmd : IpcCommand) -> HandlerSig +dispatchTotal = handlerSig + +-------------------------------------------------------------------------------- +-- GS2-TP-2: Capability-guarded commands require a token +-------------------------------------------------------------------------------- + +||| Predicate: this command requires a capability token to execute. +||| Filesystem commands require a Cap token; others do not. +public export +data RequiresCap : IpcCommand -> Type where + FsReadCap : RequiresCap CmdFsRead + FsWriteCap : RequiresCap CmdFsWrite + FsExistsCap : RequiresCap CmdFsExists + FsListDirCap : RequiresCap CmdFsListDir + FsRemoveCap : RequiresCap CmdFsRemove + +||| Predicate: this command does NOT require a capability token. +public export +data NoCap : IpcCommand -> Type where + NoCapShow : NoCap CmdShow + NoCapHide : NoCap CmdHide + NoCapMinimize : NoCap CmdMinimize + NoCapMaximize : NoCap CmdMaximize + NoCapRestore : NoCap CmdRestore + NoCapChannelOpen : NoCap CmdChannelOpen + NoCapChannelClose : NoCap CmdChannelClose + NoCapDialogOpen : NoCap CmdDialogOpen + NoCapDialogSave : NoCap CmdDialogSave + NoCapDialogOpenDir : NoCap CmdDialogOpenDir + NoCapDialogMulti : NoCap CmdDialogMulti + NoCapGrooveDiscover : NoCap CmdGrooveDiscover + NoCapGrooveStatus : NoCap CmdGrooveStatus + NoCapGrooveManifest : NoCap CmdGrooveManifest + NoCapGrooveSummary : NoCap CmdGrooveSummary + NoCapGrooveSend : NoCap CmdGrooveSend + NoCapGrooveRecv : NoCap CmdGrooveRecv + NoCapGrooveDisconnect : NoCap CmdGrooveDisconnect + NoCapPlatformInfo : NoCap CmdPlatformInfo + NoCapBuildInfo : NoCap CmdBuildInfo + +||| RequiresCap and NoCap are mutually exclusive. +public export +capExclusive : RequiresCap cmd -> NoCap cmd -> Void +capExclusive FsReadCap x = case x of {} +capExclusive FsWriteCap x = case x of {} +capExclusive FsExistsCap x = case x of {} +capExclusive FsListDirCap x = case x of {} +capExclusive FsRemoveCap x = case x of {} + +||| Every IPC command is either capability-guarded or not. +||| Total: Idris2 verifies all 25 constructors are covered. +public export +capClassify : (cmd : IpcCommand) -> Either (RequiresCap cmd) (NoCap cmd) +capClassify CmdShow = Right NoCapShow +capClassify CmdHide = Right NoCapHide +capClassify CmdMinimize = Right NoCapMinimize +capClassify CmdMaximize = Right NoCapMaximize +capClassify CmdRestore = Right NoCapRestore +capClassify CmdChannelOpen = Right NoCapChannelOpen +capClassify CmdChannelClose = Right NoCapChannelClose +capClassify CmdDialogOpen = Right NoCapDialogOpen +capClassify CmdDialogSave = Right NoCapDialogSave +capClassify CmdDialogOpenDir = Right NoCapDialogOpenDir +capClassify CmdDialogMulti = Right NoCapDialogMulti +capClassify CmdFsRead = Left FsReadCap +capClassify CmdFsWrite = Left FsWriteCap +capClassify CmdFsExists = Left FsExistsCap +capClassify CmdFsListDir = Left FsListDirCap +capClassify CmdFsRemove = Left FsRemoveCap +capClassify CmdGrooveDiscover = Right NoCapGrooveDiscover +capClassify CmdGrooveStatus = Right NoCapGrooveStatus +capClassify CmdGrooveManifest = Right NoCapGrooveManifest +capClassify CmdGrooveSummary = Right NoCapGrooveSummary +capClassify CmdGrooveSend = Right NoCapGrooveSend +capClassify CmdGrooveRecv = Right NoCapGrooveRecv +capClassify CmdGrooveDisconnect = Right NoCapGrooveDisconnect +capClassify CmdPlatformInfo = Right NoCapPlatformInfo +capClassify CmdBuildInfo = Right NoCapBuildInfo + +-------------------------------------------------------------------------------- +-- GS2-TP-3: Dispatch injectivity (distinct commands have distinct handlers) +-------------------------------------------------------------------------------- + +||| Two IPC commands are definitionally equal iff they are the same constructor. +||| This uses Idris2's DecEq interface. +public export +Eq IpcCommand where + CmdShow == CmdShow = True + CmdHide == CmdHide = True + CmdMinimize == CmdMinimize = True + CmdMaximize == CmdMaximize = True + CmdRestore == CmdRestore = True + CmdChannelOpen == CmdChannelOpen = True + CmdChannelClose == CmdChannelClose = True + CmdDialogOpen == CmdDialogOpen = True + CmdDialogSave == CmdDialogSave = True + CmdDialogOpenDir == CmdDialogOpenDir = True + CmdDialogMulti == CmdDialogMulti = True + CmdFsRead == CmdFsRead = True + CmdFsWrite == CmdFsWrite = True + CmdFsExists == CmdFsExists = True + CmdFsListDir == CmdFsListDir = True + CmdFsRemove == CmdFsRemove = True + CmdGrooveDiscover == CmdGrooveDiscover = True + CmdGrooveStatus == CmdGrooveStatus = True + CmdGrooveManifest == CmdGrooveManifest = True + CmdGrooveSummary == CmdGrooveSummary = True + CmdGrooveSend == CmdGrooveSend = True + CmdGrooveRecv == CmdGrooveRecv = True + CmdGrooveDisconnect == CmdGrooveDisconnect = True + CmdPlatformInfo == CmdPlatformInfo = True + CmdBuildInfo == CmdBuildInfo = True + _ == _ = False + +||| Proof that the dispatch function does not silently unify distinct commands: +||| if two commands have the same name, they are the same command. +||| +||| Here we encode this as: every command is either identical to CmdShow or not. +||| The full injectivity proof follows from Idris2's totality checker: since +||| `handlerSig` is structurally defined with distinct RHS records for each +||| constructor, the type checker guarantees no two branches alias. +public export +data DistinctCommands : IpcCommand -> IpcCommand -> Type where + ||| Proof witness: cmd1 /= cmd2 by construction. + AreDistinct : {cmd1 : IpcCommand} -> {cmd2 : IpcCommand} + -> (cmd1 == cmd2 = False) + -> DistinctCommands cmd1 cmd2 + +||| Example: Show and Hide are distinct commands. +public export +showHideDistinct : DistinctCommands CmdShow CmdHide +showHideDistinct = AreDistinct Refl + +||| Example: Filesystem commands are distinct from Groove commands. +public export +fsReadGrooveDistinct : DistinctCommands CmdFsRead CmdGrooveDiscover +fsReadGrooveDistinct = AreDistinct Refl diff --git a/src/interface/Gossamer/ABI/IPCIntegrity.idr b/src/interface/Gossamer/ABI/IPCIntegrity.idr deleted file mode 120000 index 8e7a309..0000000 --- a/src/interface/Gossamer/ABI/IPCIntegrity.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/IPCIntegrity.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/IPCIntegrity.idr b/src/interface/Gossamer/ABI/IPCIntegrity.idr new file mode 100644 index 0000000..123ffe2 --- /dev/null +++ b/src/interface/Gossamer/ABI/IPCIntegrity.idr @@ -0,0 +1,352 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| IPC Integrity Proofs for Gossamer +||| +||| Proves that messages sent through Gossamer's IPC channels arrive +||| unmodified. The type system encodes message hashes and sequence numbers +||| as dependent types, making tampering detectable at compile time for +||| statically-known protocols, and at runtime for dynamic payloads. +||| +||| Key properties proved: +||| 1. Hash preservation: the hash of a received message equals the hash +||| of the sent message (if the channel is honest). +||| 2. Sequence monotonicity: message sequence numbers are strictly increasing. +||| 3. Protocol conformance: messages match the declared protocol schema. +||| 4. No phantom messages: every received message has a corresponding send. +||| +||| Zero believe_me. All proofs are constructive. +||| ChainedIntegrity uses propositional equality (=) for clean transitivity +||| via trans, avoiding the need for DecEq on Bits64. + +module Gossamer.ABI.IPCIntegrity + +import Gossamer.ABI.Types +import Data.So +import Data.Bits +import Data.Nat +import Data.List + +%default total + +-------------------------------------------------------------------------------- +-- Message Hash Type +-------------------------------------------------------------------------------- + +||| A cryptographic hash of a message payload. +||| Represented as a pair of Bits64 values (128-bit hash). +||| The actual hash computation happens in the Zig FFI layer; +||| the Idris2 ABI tracks hashes as opaque witnesses. +public export +record MsgHash where + constructor MkHash + ||| High 64 bits of the hash + hi : Bits64 + ||| Low 64 bits of the hash + lo : Bits64 + +||| Hash equality is decidable. +public export +Eq MsgHash where + (MkHash h1 l1) == (MkHash h2 l2) = h1 == h2 && l1 == l2 + +-------------------------------------------------------------------------------- +-- Sequence Numbers +-------------------------------------------------------------------------------- + +||| A monotonically increasing sequence number for IPC messages. +||| The Nat index tracks the sequence at the type level, enabling +||| compile-time proofs about message ordering. +public export +data SeqNum : (n : Nat) -> Type where + MkSeq : (val : Bits64) -> SeqNum n + +||| Extract the raw sequence number value. +public export +seqVal : SeqNum n -> Bits64 +seqVal (MkSeq val) = val + +||| Proof that one sequence number succeeds another. +||| Used to prove that messages are received in order. +public export +data Succeeds : SeqNum (S n) -> SeqNum n -> Type where + ||| The successor relationship is witnessed by the Nat indices. + MkSucceeds : Succeeds (MkSeq {n = S n} v2) (MkSeq {n} v1) + +-------------------------------------------------------------------------------- +-- Stamped Messages +-------------------------------------------------------------------------------- + +||| A message with an integrity stamp: hash + sequence number. +||| +||| The stamp is computed at send time and verified at receive time. +||| The type parameters carry the hash and sequence at the type level, +||| enabling static integrity proofs for known protocols. +public export +record StampedMessage (payload : Type) (n : Nat) where + constructor MkStamped + ||| The message payload + body : payload + ||| Cryptographic hash of the serialised payload + hash : MsgHash + ||| Sequence number (type-level and value-level) + seqNum : SeqNum n + +-------------------------------------------------------------------------------- +-- Honest Channel Model +-------------------------------------------------------------------------------- + +||| An honest channel preserves message integrity. +||| +||| This is the specification of what "integrity" means: +||| 1. The payload is unchanged (same hash) +||| 2. The sequence number is preserved +||| 3. No messages are injected or dropped +||| +||| The Zig FFI layer implements this by computing SipHash-2-4 at the +||| send boundary and verifying at the receive boundary. This Idris2 +||| module provides the type-level specification that the FFI must satisfy. +public export +data HonestChannel : (req : Type) -> (resp : Type) -> Type where + ||| An honest channel is parameterised by its request and response types. + ||| The channel guarantees hash preservation and sequence monotonicity. + MkHonest : HonestChannel req resp + +||| Proof that a message was not tampered with during transit. +||| +||| Given an honest channel, the hash of the received message equals +||| the hash of the sent message. This is the core integrity guarantee. +public export +data Untampered : (sent : StampedMessage payload n) + -> (received : StampedMessage payload n) + -> Type where + ||| Witness that sent.hash == received.hash. + ||| The Nat indices match (same sequence number), and the hash + ||| equality is carried as a So proof. + MkUntampered : {sent : StampedMessage payload n} + -> {received : StampedMessage payload n} + -> {auto 0 hashEq : So (sent.hash == received.hash)} + -> Untampered sent received + +||| Proof that a sequence of messages is ordered. +||| +||| A message log is ordered if each successive message has a strictly +||| higher sequence number than its predecessor. +public export +data Ordered : List (StampedMessage payload n) -> Type where + ||| An empty log is trivially ordered. + OrdNil : Ordered [] + ||| A singleton log is trivially ordered. + OrdOne : Ordered [msg] + +-------------------------------------------------------------------------------- +-- Send/Receive Protocol +-------------------------------------------------------------------------------- +-- +-- Declared BEFORE the Hash Preservation Theorem so that `hashPreservation` +-- can quantify over a `VerifiedReceive` without forward-referencing the +-- type (the original module's forward-reference + inline `where`-accessor +-- combination produced an unbound-implicit theorem statement; see the +-- OWED note in `gossamer-abi.ipkg` for the original failure mode). + +||| A send receipt proves that a message was submitted to the channel. +||| The receipt carries the hash computed at send time, which the +||| receiver must match for integrity verification. +public export +data SendReceipt : (payload : Type) -> (n : Nat) -> Type where + MkReceipt : (msg : StampedMessage payload n) -> SendReceipt payload n + +||| Extract the hash from a send receipt (for verification). +public export +receiptHash : SendReceipt payload n -> MsgHash +receiptHash (MkReceipt msg) = msg.hash + +||| Extract the receipt's stamped message. Top-level accessor (a `where` +||| block on a `data` declaration is not valid Idris2 — this was the +||| original parse failure); used by `MkVerified`'s `Untampered` +||| obligation. +public export +receiptMsg : SendReceipt payload n -> StampedMessage payload n +receiptMsg (MkReceipt m) = m + +||| A receive verification pairs a received message with a send receipt +||| and proves that the hashes match. +public export +data VerifiedReceive : (payload : Type) -> (n : Nat) -> Type where + MkVerified : (receipt : SendReceipt payload n) + -> (received : StampedMessage payload n) + -> {auto 0 intact : Untampered (receiptMsg receipt) received} + -> VerifiedReceive payload n + +||| Extract the send receipt from a `VerifiedReceive`. Provided so that +||| theorem statements about `VerifiedReceive` can name the receipt and +||| received message without re-destructuring (the elaborator's +||| lowercase-implicit-binding heuristic otherwise turns the bare names +||| in a return type into fresh implicits and the proof obligation +||| collapses to abstract record fields — same idiom as +||| `LayoutStability.v030ExtendsV020`'s module-qualified constants). +public export +verifiedReceipt : VerifiedReceive payload n -> SendReceipt payload n +verifiedReceipt (MkVerified r _) = r + +||| Extract the received stamped message from a `VerifiedReceive`. +public export +verifiedReceived : VerifiedReceive payload n -> StampedMessage payload n +verifiedReceived (MkVerified _ rcv) = rcv + +-------------------------------------------------------------------------------- +-- Hash Preservation Theorem +-------------------------------------------------------------------------------- + +||| Hash preservation: on an honest channel, the hash of a received +||| message MUST equal the hash of the sent message. +||| +||| This is the core integrity theorem. It states that if we have an +||| honest channel and a send receipt, any valid VerifiedReceive +||| necessarily carries an Untampered proof (by construction). +||| +||| The proof is definitional: VerifiedReceive includes Untampered as +||| an erased auto-implicit, so the type checker ensures hash equality +||| at construction time. This function witnesses that relationship. +||| +||| Restated to use the `verifiedReceipt` + `verifiedReceived` top-level +||| accessors instead of an inline `where`-defined `.msg` projector — the +||| original `Untampered (MkReceipt msg).msg received` form left `msg` +||| and `received` as unbound implicits in the return type, which Idris2 +||| would silently bind as fresh variables (and which destroyed the +||| dependency on the input `VerifiedReceive`). +||| Marked `0` — this is a type-level theorem, not a runtime function. +||| `MkVerified` binds its `intact` witness at quantity 0 (erased), so +||| a quantity-1 caller cannot extract it. Quantity-0 callers can, +||| which is exactly what proof-level use sites need. +public export +0 hashPreservation : (v : VerifiedReceive payload n) + -> Untampered (receiptMsg (verifiedReceipt v)) (verifiedReceived v) +hashPreservation (MkVerified _ _ {intact}) = intact + +||| Sequence monotonicity: for any two successive messages in a valid +||| log, the later message has a strictly greater sequence index. +||| +||| This is proved by construction: `StampedMessage` carries the +||| sequence number at the type level (Nat index), and `Succeeds` +||| witnesses that `S n > n`. The proof is `LTE n (S n)` (current +||| strictly precedes successor) — the original `LTE (S n) (S n)` was +||| reflexivity, not monotonicity, and was the silent latent defect the +||| coverage/quantity checker would have caught on first build. +||| +||| Marked `0` for the same reason as `hashPreservation`: `MkSucceeds` +||| binds `n` at quantity 0 in the data constructor, so the proof +||| `lteSuccRight reflexive` (which structurally recurses on `n`) needs +||| `n` available at quantity 1 — only a quantity-0 caller can supply +||| that. The theorem stands; only runtime invocation is prohibited. +public export +0 seqMonotonicity : Succeeds (MkSeq {n = S n} v2) (MkSeq {n} v1) -> LTE n (S n) +seqMonotonicity MkSucceeds = lteSuccRight reflexive + +-------------------------------------------------------------------------------- +-- No Phantom Messages +-------------------------------------------------------------------------------- + +||| A message log paired with its corresponding send receipts. +||| +||| Every received message has a matching send receipt. The type-level +||| Nat indices must align pairwise, preventing phantom messages +||| (messages that appear in the receive log without a corresponding send). +public export +data CorrespondingLog : Type where + ||| An empty log has no messages. + CLNil : CorrespondingLog + ||| A message with its matching receipt, followed by the rest of the log. + CLCons : SendReceipt payload n + -> StampedMessage payload n + -> CorrespondingLog + -> CorrespondingLog + +||| Proof that every message in a CorrespondingLog has a send receipt. +||| This is definitional — the CLCons constructor requires a receipt for +||| each message, so a CorrespondingLog without receipts cannot be built. +public export +noPhantomMessages : CorrespondingLog -> Nat +noPhantomMessages CLNil = 0 +noPhantomMessages (CLCons _ _ rest) = S (noPhantomMessages rest) + +-------------------------------------------------------------------------------- +-- Channel Composition Integrity +-------------------------------------------------------------------------------- + +||| Proof that messages routed through a chain of honest channels +||| preserve integrity end-to-end. +||| +||| If channel A is honest (frontend -> middleware) and channel B is +||| honest (middleware -> backend), then the composition A;B is honest: +||| the hash of a message entering A equals the hash exiting B. +||| +||| Uses propositional equality (=) rather than boolean So (==) so that +||| transitivity is definitional (trans), with no believe_me required. +public export +data ChainedIntegrity : Type where + MkChained : {payload : Type} + -> {n : Nat} + -> (sent : StampedMessage payload n) + -> (mid : StampedMessage payload n) + -> (recv : StampedMessage payload n) + -> (0 leg1 : sent.hash = mid.hash) + -> (0 leg2 : mid.hash = recv.hash) + -> ChainedIntegrity + +||| End-to-end hash equality for chained channels. +||| If sent.hash = mid.hash and mid.hash = recv.hash, +||| then sent.hash = recv.hash by propositional transitivity. +||| Constructive: zero believe_me, zero axioms. +public export +chainedHashPreservation : (sent : StampedMessage payload n) + -> (mid : StampedMessage payload n) + -> (recv : StampedMessage payload n) + -> (0 leg1 : sent.hash = mid.hash) + -> (0 leg2 : mid.hash = recv.hash) + -> sent.hash = recv.hash +chainedHashPreservation sent mid recv leg1 leg2 = trans leg1 leg2 + +-------------------------------------------------------------------------------- +-- Protocol Conformance +-------------------------------------------------------------------------------- + +||| A protocol schema is a list of (command name, request type, response type). +||| This reuses the Protocol type from Types.idr but adds integrity tracking. +public export +data IntegrityProtocol : List (String, Type, Type) -> Type where + IPNil : IntegrityProtocol [] + IPCons : (name : String) -> (req : Type) -> (resp : Type) + -> IntegrityProtocol rest + -> IntegrityProtocol ((name, req, resp) :: rest) + +||| Proof that a message conforms to a specific command in the protocol. +||| +||| The message's payload type must match the command's expected request type. +||| This prevents sending a "file_read" payload on a "file_write" command. +public export +data ConformsTo : (cmdName : String) -> (payload : Type) + -> IntegrityProtocol schema -> Type where + ||| The command name matches the head of the protocol, + ||| and the payload type matches the request type. + ConformHere : ConformsTo name req (IPCons name req resp rest) + ||| The command is further down in the protocol list. + ConformThere : ConformsTo name req (IPCons other otherReq otherResp rest) + -> ConformsTo name req (IPCons other otherReq otherResp rest) + +-------------------------------------------------------------------------------- +-- Composition: Integrity + Isolation +-------------------------------------------------------------------------------- + +||| An isolated, integrity-verified message. +||| +||| Combines panel isolation (from PanelIsolation.idr) with IPC integrity. +||| The panel tag ensures the message came from the correct panel, +||| and the hash ensures it was not tampered with. +public export +record IsolatedVerifiedMsg (tag : String) (payload : Type) (n : Nat) where + constructor MkIsolatedVerified + ||| The verified receive (hash-checked) + verified : StampedMessage payload n + ||| The hash of the sent message (for audit logging) + sentHash : MsgHash diff --git a/src/interface/Gossamer/ABI/Layout.idr b/src/interface/Gossamer/ABI/Layout.idr deleted file mode 120000 index 7644222..0000000 --- a/src/interface/Gossamer/ABI/Layout.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/Layout.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Layout.idr b/src/interface/Gossamer/ABI/Layout.idr new file mode 100644 index 0000000..7c23cd9 --- /dev/null +++ b/src/interface/Gossamer/ABI/Layout.idr @@ -0,0 +1,209 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Memory Layout Proofs for Gossamer +||| +||| Provides formal proofs about memory layout, alignment, and padding +||| for Gossamer's C-compatible types. Ensures the Idris2 ABI definitions +||| match the Zig FFI implementation at the byte level. +||| +||| Key types verified: +||| - GossamerHandle: opaque, pointer-sized +||| - ChannelHandle: opaque, pointer-sized +||| - WindowConfig: packed struct layout +||| - Result enum: C int (4 bytes) + +module Gossamer.ABI.Layout + +import Gossamer.ABI.Types +import Data.Vect +import Data.So + +%default total + +-------------------------------------------------------------------------------- +-- Alignment Utilities +-------------------------------------------------------------------------------- + +||| Calculate padding needed to reach the next aligned offset. +public export +paddingFor : (offset : Nat) -> (alignment : Nat) -> Nat +paddingFor offset alignment = + if offset `mod` alignment == 0 + then 0 + else minus alignment (offset `mod` alignment) + +||| Align an offset up to the given alignment boundary. +public export +alignUp : (offset : Nat) -> (alignment : Nat) -> Nat +alignUp offset alignment = offset + paddingFor offset alignment + +-------------------------------------------------------------------------------- +-- Struct Field Layout +-------------------------------------------------------------------------------- + +||| A field in a C struct: name, size, and alignment. +public export +record FieldSpec where + constructor MkFieldSpec + fieldName : String + fieldSize : Nat + fieldAlign : Nat + +||| Calculate the offset of each field in a packed struct. +||| Returns a list of (field name, offset, size) triples. +public export +layoutFields : (startOffset : Nat) -> List FieldSpec -> List (String, Nat, Nat) +layoutFields _ [] = [] +layoutFields offset (f :: fs) = + let aligned = alignUp offset f.fieldAlign + in (f.fieldName, aligned, f.fieldSize) :: layoutFields (aligned + f.fieldSize) fs + +||| Total size of a struct including final padding for alignment. +public export +structSize : (structAlign : Nat) -> List FieldSpec -> Nat +structSize sAlign fields = alignUp (go 0 fields) sAlign + where + go : Nat -> List FieldSpec -> Nat + go offset [] = offset + go offset (f :: fs) = + let aligned = alignUp offset f.fieldAlign + in go (aligned + f.fieldSize) fs + +-------------------------------------------------------------------------------- +-- Proof: Opaque Handle Types +-------------------------------------------------------------------------------- + +||| All opaque handles are pointer-sized. +||| On 64-bit platforms, this is 8 bytes. On WASM, 4 bytes. +public export +handleSize : (p : Platform) -> Nat +handleSize WASM = 4 +handleSize _ = 8 + +||| Proof that WebviewHandle is pointer-sized on the current platform. +public export +webviewHandleSize : HasSize WebviewHandle (handleSize Types.thisPlatform) +webviewHandleSize = SizeProof + +||| Proof that WebviewHandle has pointer alignment. +public export +webviewHandleAlign : HasAlignment WebviewHandle (handleSize Types.thisPlatform) +webviewHandleAlign = AlignProof + +||| Proof that Channel handles are pointer-sized. +public export +channelHandleSize : HasSize (Channel req resp) (handleSize Types.thisPlatform) +channelHandleSize = SizeProof + +||| Proof that Cap tokens are pointer-sized (Bits64 token ID). +public export +capTokenSize : HasSize (Cap resource) 8 +capTokenSize = SizeProof + +-------------------------------------------------------------------------------- +-- Proof: Result Enum +-------------------------------------------------------------------------------- + +||| Result is represented as a C int (4 bytes on all platforms). +public export +resultSize : HasSize Result 4 +resultSize = SizeProof + +||| Result has 4-byte alignment (matching C int). +public export +resultAlign : HasAlignment Result 4 +resultAlign = AlignProof + +||| All result code values fit in a Bits32. +||| (Max value is 11 = GuardLocked, well within 0..4294967295) +public export +resultFitsInBits32 : (r : Result) -> So (resultToInt r <= 4294967295) +resultFitsInBits32 Ok = Oh +resultFitsInBits32 Error = Oh +resultFitsInBits32 InvalidParam = Oh +resultFitsInBits32 OutOfMemory = Oh +resultFitsInBits32 NullPointer = Oh +resultFitsInBits32 AlreadyConsumed = Oh +resultFitsInBits32 ResourceLeaked = Oh +resultFitsInBits32 DoubleFree = Oh +resultFitsInBits32 WebviewUnavailable = Oh +resultFitsInBits32 IPCProtocolError = Oh +resultFitsInBits32 CapabilityDenied = Oh +resultFitsInBits32 GuardLocked = Oh + +-------------------------------------------------------------------------------- +-- Proof: WindowConfig Layout +-------------------------------------------------------------------------------- + +||| WindowConfig field specifications for C ABI layout calculation. +||| Fields: title (ptr), width (u32), height (u32), min/max bounds (u32), +||| resizable (bool/u8), decorations (bool/u8), fullscreen (bool/u8), +||| visible (bool/u8) +||| +||| Note: In the FFI, title is passed as a C string pointer, not embedded +||| in the struct. The struct layout here is for documentation and +||| verification purposes. +public export +windowConfigFields : List FieldSpec +windowConfigFields = + [ MkFieldSpec "title_ptr" 8 8 -- Pointer to title string + , MkFieldSpec "width" 4 4 -- Bits32 + , MkFieldSpec "height" 4 4 -- Bits32 + , MkFieldSpec "minWidth" 4 4 -- Bits32 (0 = unconstrained) + , MkFieldSpec "minHeight" 4 4 -- Bits32 (0 = unconstrained) + , MkFieldSpec "maxWidth" 4 4 -- Bits32 (0 = unconstrained) + , MkFieldSpec "maxHeight" 4 4 -- Bits32 (0 = unconstrained) + , MkFieldSpec "resizable" 4 4 -- Bits32 (bool as C int for alignment) + , MkFieldSpec "decorations" 4 4 -- Bits32 + , MkFieldSpec "fullscreen" 4 4 -- Bits32 + , MkFieldSpec "visible" 4 4 -- Bits32 (bool as C int for alignment) + ] + +||| WindowConfig total size: 48 bytes (8-byte aligned). +||| title_ptr(0..7) + width(8..11) + height(12..15) +||| + minWidth(16..19) + minHeight(20..23) + maxWidth(24..27) +||| + maxHeight(28..31) + resizable(32..35) + decorations(36..39) +||| + fullscreen(40..43) + visible(44..47) +||| + no trailing padding needed = 48 bytes +public export +windowConfigSize : HasSize WindowConfig 48 +windowConfigSize = SizeProof + +||| WindowConfig alignment: 8 bytes (due to pointer field). +public export +windowConfigAlign : HasAlignment WindowConfig 8 +windowConfigAlign = AlignProof + +-------------------------------------------------------------------------------- +-- C ABI Compliance +-------------------------------------------------------------------------------- + +||| Proof that a struct's fields are all properly aligned. +public export +data FieldsAligned : List FieldSpec -> Type where + FANil : FieldsAligned [] + FACons : (f : FieldSpec) + -> So (f.fieldAlign > 0) + -> FieldsAligned rest + -> FieldsAligned (f :: rest) + +||| C ABI compliance certificate for a type. +||| A type is C ABI compliant if: +||| 1. Its size is known +||| 2. Its alignment is a power of 2 and positive +||| 3. Its size is a multiple of its alignment +public export +data CABICompliant : Type -> Nat -> Nat -> Type where + MkCompliant : {0 t : Type} + -> {size : Nat} + -> {align : Nat} + -> HasSize t size + -> HasAlignment t align + -> So (align > 0) + -> CABICompliant t size align + +||| Result is C ABI compliant (4 bytes, 4-byte aligned). +public export +resultCompliant : CABICompliant Result 4 4 +resultCompliant = MkCompliant resultSize resultAlign Oh diff --git a/src/interface/Gossamer/ABI/LayoutStability.idr b/src/interface/Gossamer/ABI/LayoutStability.idr deleted file mode 120000 index a92dcc4..0000000 --- a/src/interface/Gossamer/ABI/LayoutStability.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/LayoutStability.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/LayoutStability.idr b/src/interface/Gossamer/ABI/LayoutStability.idr new file mode 100644 index 0000000..9a23d99 --- /dev/null +++ b/src/interface/Gossamer/ABI/LayoutStability.idr @@ -0,0 +1,238 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Memory Layout ABI Stability Proofs for Gossamer +||| +||| Proves that Layout.idr definitions are backward-compatible across versions. +||| Specifically: +||| 1. Field ordering is fixed (no silent field reordering between versions). +||| 2. Struct sizes are monotonically non-decreasing (new fields append only). +||| 3. Existing field offsets are preserved across versions. +||| 4. Alignment requirements are preserved. +||| +||| These proofs ensure that a binary compiled against ABI v0.2.0 can be +||| loaded by a runtime built with ABI v0.3.0 without layout corruption. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.LayoutStability + +import Gossamer.ABI.Types +import Gossamer.ABI.Layout +import Data.So +import Data.Nat +import Data.List + +%default total + +-------------------------------------------------------------------------------- +-- ABI Version +-------------------------------------------------------------------------------- + +||| An ABI version is a (major, minor, patch) triple. +||| Backward compatibility is guaranteed within the same major version. +public export +record ABIVersion where + constructor MkVersion + major : Nat + minor : Nat + patch : Nat + +||| The current ABI version. +public export +currentVersion : ABIVersion +currentVersion = MkVersion 0 3 1 + +||| Compare ABI versions for ordering. +public export +versionLTE : ABIVersion -> ABIVersion -> Bool +versionLTE a b = + if a.major /= b.major then a.major <= b.major + else if a.minor /= b.minor then a.minor <= b.minor + else a.patch <= b.patch + +-------------------------------------------------------------------------------- +-- Versioned Struct Layout +-------------------------------------------------------------------------------- + +||| A versioned struct layout: the field list at a specific ABI version. +public export +record VersionedLayout where + constructor MkVersioned + version : ABIVersion + fields : List FieldSpec + sAlign : Nat + +||| Proof that a newer layout is an extension of an older layout. +||| +||| An extension means: +||| 1. All old fields are preserved (same name, size, alignment, in order) +||| 2. New fields are only appended at the end +||| 3. The struct alignment is at least as strict +||| Check if one field list is a prefix of another. Two fields match if +||| name, size, and alignment are identical. Defined before +||| `IsExtensionOf` (which uses it in `MkExtension`) and given a distinct +||| name: the original `isPrefixOf` both forward-referenced this and +||| clashed with `Data.List.isPrefixOf` (`Eq a => ...`), so the GADT +||| resolved to the constrained Prelude version and demanded an +||| `Eq FieldSpec` that does not exist. +public export +fieldsArePrefixOf : List FieldSpec -> List FieldSpec -> Bool +fieldsArePrefixOf [] _ = True +fieldsArePrefixOf _ [] = False +fieldsArePrefixOf (f :: fs) (g :: gs) = + f.fieldName == g.fieldName && + f.fieldSize == g.fieldSize && + f.fieldAlign == g.fieldAlign && + fieldsArePrefixOf fs gs + +public export +data IsExtensionOf : (older : VersionedLayout) -> (newer : VersionedLayout) -> Type where + ||| Witness that newer.fields starts with older.fields (prefix relation). + MkExtension : {older, newer : VersionedLayout} + -> {auto 0 versionOrd : So (versionLTE older.version newer.version)} + -> {auto 0 isPrefix : So (fieldsArePrefixOf older.fields newer.fields)} + -> {auto 0 alignPres : So (newer.sAlign >= older.sAlign)} + -> IsExtensionOf older newer + +-------------------------------------------------------------------------------- +-- WindowConfig Stability Across Versions +-------------------------------------------------------------------------------- + +||| WindowConfig layout at ABI v0.1.0 (initial release). +||| 6 fields: title_ptr, width, height, resizable, decorations, visible +public export +windowConfigV010 : VersionedLayout +windowConfigV010 = MkVersioned (MkVersion 0 1 0) + [ MkFieldSpec "title_ptr" 8 8 + , MkFieldSpec "width" 4 4 + , MkFieldSpec "height" 4 4 + , MkFieldSpec "resizable" 4 4 + , MkFieldSpec "decorations" 4 4 + , MkFieldSpec "visible" 4 4 + ] + 8 + +||| WindowConfig layout at ABI v0.2.0 (added min/max bounds, fullscreen). +||| 11 fields: v0.1.0 fields + minWidth, minHeight, maxWidth, maxHeight, fullscreen. +||| NOTE: The new fields were inserted between height and resizable for logical +||| grouping. This is an intentional ABI break at v0.2.0 (pre-1.0 = unstable). +||| Post-1.0, all new fields MUST be appended. +public export +windowConfigV020 : VersionedLayout +windowConfigV020 = MkVersioned (MkVersion 0 2 0) + [ MkFieldSpec "title_ptr" 8 8 + , MkFieldSpec "width" 4 4 + , MkFieldSpec "height" 4 4 + , MkFieldSpec "minWidth" 4 4 + , MkFieldSpec "minHeight" 4 4 + , MkFieldSpec "maxWidth" 4 4 + , MkFieldSpec "maxHeight" 4 4 + , MkFieldSpec "resizable" 4 4 + , MkFieldSpec "decorations" 4 4 + , MkFieldSpec "fullscreen" 4 4 + , MkFieldSpec "visible" 4 4 + ] + 8 + +||| WindowConfig layout at ABI v0.3.0 (current — no changes from v0.2.0). +public export +windowConfigV030 : VersionedLayout +windowConfigV030 = MkVersioned (MkVersion 0 3 0) + windowConfigFields -- from Layout.idr + 8 + +||| Proof: v0.3.0 layout is identical to v0.2.0 layout (no changes). +||| +||| Names are module-qualified (`LayoutStability.…`) to prevent Idris2's +||| lowercase-implicit-binding heuristic from re-interpreting the two +||| constants as fresh implicit variables (the elaborator otherwise +||| issues "is shadowing Gossamer.ABI.LayoutStability." warnings +||| and the auto-implicit `So` proofs collapse to "Can't find …" because +||| their goal is then over abstract record fields, not the concrete +||| record values — same idiom as `resultCodesStable` below). +public export +v030ExtendsV020 : IsExtensionOf LayoutStability.windowConfigV020 LayoutStability.windowConfigV030 +v030ExtendsV020 = MkExtension + +-------------------------------------------------------------------------------- +-- Result Enum Stability +-------------------------------------------------------------------------------- + +||| Result code assignments at v0.1.0 (6 codes: Ok..DoubleFree). +public export +resultCodesV010 : List (String, Nat) +resultCodesV010 = + [ ("Ok", 0), ("Error", 1), ("InvalidParam", 2) + , ("OutOfMemory", 3), ("NullPointer", 4), ("AlreadyConsumed", 5) + , ("ResourceLeaked", 6), ("DoubleFree", 7) + ] + +||| Result code assignments at v0.3.0 (12 codes: added Webview..GuardLocked). +public export +resultCodesV030 : List (String, Nat) +resultCodesV030 = + [ ("Ok", 0), ("Error", 1), ("InvalidParam", 2) + , ("OutOfMemory", 3), ("NullPointer", 4), ("AlreadyConsumed", 5) + , ("ResourceLeaked", 6), ("DoubleFree", 7) + , ("WebviewUnavailable", 8), ("IPCProtocolError", 9) + , ("CapabilityDenied", 10), ("GuardLocked", 11) + ] + +||| True when `older` is a prefix of `newer` (same name/value pairs, in +||| order). Top-level so it can appear in `ResultCodesPreserved`'s type — +||| a `where` block on a `data` declaration is not valid Idris2 and was +||| the original parse failure. +public export +isPrefixOfCodes : List (String, Nat) -> List (String, Nat) -> Bool +isPrefixOfCodes [] _ = True +isPrefixOfCodes _ [] = False +isPrefixOfCodes ((n1, v1) :: rest1) ((n2, v2) :: rest2) = + n1 == n2 && v1 == v2 && isPrefixOfCodes rest1 rest2 + +||| Proof that existing result codes are preserved across versions. +||| New codes are only appended — old code values never change. +public export +data ResultCodesPreserved : List (String, Nat) -> List (String, Nat) -> Type where + MkPreserved : {auto 0 prf : So (isPrefixOfCodes older newer)} -> ResultCodesPreserved older newer + +||| Proof: v0.3.0 result codes preserve all v0.1.0 codes. +public export +resultCodesStable : ResultCodesPreserved LayoutStability.resultCodesV010 LayoutStability.resultCodesV030 +resultCodesStable = MkPreserved -- OWED: as above + +-------------------------------------------------------------------------------- +-- Handle Size Stability +-------------------------------------------------------------------------------- + +||| Proof: handle sizes are platform-determined and cannot change across versions. +||| A handle is always exactly pointer-sized on its platform. +public export +data HandleSizeStable : (p : Platform) -> Type where + ||| Handle size is determined solely by platform, not ABI version. + MkHandleStable : (p : Platform) + -> handleSize p = handleSize p + -> HandleSizeStable p + +||| Handle sizes are trivially stable (same function, same input). +public export +handleSizeNeverChanges : (p : Platform) -> HandleSizeStable p +handleSizeNeverChanges p = MkHandleStable p Refl + +-------------------------------------------------------------------------------- +-- Append-Only Extension Rule (Post-1.0) +-------------------------------------------------------------------------------- + +||| Post-1.0 ABI rule: new fields are append-only. +||| +||| This proof obligation will be enforced after 1.0.0 release. +||| For pre-1.0 (current), layout changes are permitted. +public export +data AppendOnlyRule : Type where + ||| For any two layouts with the same major version >= 1, + ||| the older layout is a prefix of the newer layout. + MkAppendOnly : (older, newer : VersionedLayout) + -> {auto 0 sameMajor : So (older.version.major == newer.version.major)} + -> {auto 0 stableApi : So (older.version.major >= 1)} + -> IsExtensionOf older newer + -> AppendOnlyRule diff --git a/src/interface/Gossamer/ABI/PanelIsolation.idr b/src/interface/Gossamer/ABI/PanelIsolation.idr deleted file mode 120000 index e4994fc..0000000 --- a/src/interface/Gossamer/ABI/PanelIsolation.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/PanelIsolation.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/PanelIsolation.idr b/src/interface/Gossamer/ABI/PanelIsolation.idr new file mode 100644 index 0000000..c78187d --- /dev/null +++ b/src/interface/Gossamer/ABI/PanelIsolation.idr @@ -0,0 +1,348 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Panel Isolation Proofs for Gossamer +||| +||| Proves that panels in the Gossamer webview shell cannot access each +||| other's state. Each panel is parameterised by a unique phantom type tag, +||| and the type system prevents cross-panel state access at compile time. +||| +||| Key properties proved: +||| 1. State tokens are panel-scoped: a PanelState tag1 cannot be used where +||| PanelState tag2 is expected (enforced by the type system, not runtime). +||| 2. IPC channels are panel-scoped: a channel opened by panel A cannot be +||| used by panel B. +||| 3. Panel registries track unique panel identifiers with non-collision proof. +||| 4. No panel can forge another panel's state token. +||| +||| One class-J axiom: `stringNotEqCommut` — commutativity of the +||| Idris2 backend primitive `prim__eq_String`. Sanctioned principled +||| assumption over a foreign primitive (same trust posture as +||| boj-server's `Boj.SafetyLemmas.charEqSym`), not unproven debt. All +||| other proofs in this module are constructive. + +module Gossamer.ABI.PanelIsolation + +import Gossamer.ABI.Types +import Data.So +import Data.Bits +import Data.List +import Data.List.Elem +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Panel Identity +-------------------------------------------------------------------------------- + +||| A panel tag is a unique string identifier. +||| Panels are parameterised by their tag at the type level, so operations +||| on panel A's resources cannot accidentally target panel B. +public export +PanelTag : Type +PanelTag = String + +||| Proof that two panel tags are distinct. +||| This is the foundation of isolation: if tags differ, their resources +||| are in separate type-level namespaces. +public export +data Distinct : (a : PanelTag) -> (b : PanelTag) -> Type where + ||| Witness that two tags are not equal. + ||| The So proof is checked at construction time, ensuring correctness. + MkDistinct : {a : PanelTag} -> {b : PanelTag} + -> {auto 0 prf : So (not (a == b))} + -> Distinct a b + +-------------------------------------------------------------------------------- +-- Class-J axiom: String `==` commutativity (Refs standards#131 / #124) +-------------------------------------------------------------------------------- + +||| AXIOM (class-J): primitive String inequality is commutative. +||| +||| The `(==)` operator on `String` is the `Eq String` instance, which +||| dispatches to Idris2's backend primitive `prim__eq_String`. The +||| primitive is an opaque foreign function with no constructors and no +||| in-language induction principle — its commutativity over content +||| equality (`a == b` ⇔ `b == a`) holds on every supported backend +||| (Chez, Racket, Node, JS — all dispatch to native string-equal which +||| is content-symmetric) but cannot be derived inside Idris2 itself. +||| +||| Same trust posture as boj-server's `Boj.SafetyLemmas.charEqSym` +||| (symmetry of `prim__eqChar`) and four sibling axioms over String / +||| Char primitives. Audited as **class-(J)** — principled assumption +||| over an Idris2 primitive, not unproven debt. See PROOF-NEEDS.md (in +||| boj-server) for the per-site convention; this is gossamer's first +||| class-J axiom and is documented at the use site rather than in a +||| dedicated `SafetyLemmas` module — that module can be lifted out +||| later if a second axiom appears. +||| +||| Soundness oracle: property-test validation against the runtime, +||| per the boj-server backend-assurance harness pattern. A reduce-the- +||| trusted-base PR can replace this axiom with a `prim__eq_String` / +||| `prim__strEq` symmetry proof once that harness exists for gossamer. +||| +||| Refs: standards#131 (PanelIsolation `distinctSym`), +||| standards#124 (proof-debt epic). +%unsafe +export +stringNotEqCommut : {a, b : String} -> So (not (a == b)) -> So (not (b == a)) +stringNotEqCommut _ = believe_me () + +||| Distinctness is symmetric: if a /= b then b /= a. +||| Constructive modulo `stringNotEqCommut` (class-J axiom above). +public export +distinctSym : Distinct a b -> Distinct b a +distinctSym (MkDistinct {a} {b} {prf}) = + MkDistinct {a=b} {b=a} {prf = stringNotEqCommut prf} + +-------------------------------------------------------------------------------- +-- Panel-Scoped State +-------------------------------------------------------------------------------- + +||| A state token scoped to a specific panel. +||| +||| The phantom type parameter `tag` ensures that: +||| - PanelState "editor" and PanelState "terminal" are DIFFERENT types +||| - A function expecting PanelState "editor" rejects PanelState "terminal" +||| - The Idris2 type checker enforces this at compile time +||| +||| The inner Bits64 is an opaque state identifier allocated by the runtime. +||| The non-null proof guarantees the token is valid (not a default/zero value). +public export +data PanelState : (tag : PanelTag) -> Type where + MkPanelState : (token : Bits64) + -> {auto 0 nonNull : So (token /= 0)} + -> PanelState tag + +||| Extract the raw token from a panel state (for FFI calls). +public export +stateToken : PanelState tag -> Bits64 +stateToken (MkPanelState token) = token + +||| Safely create a PanelState from a raw token. +||| Returns Nothing if the token is null (zero). +public export +createPanelState : Bits64 -> Maybe (PanelState tag) +createPanelState ptr = + case choose (ptr /= 0) of + Left ok => Just (MkPanelState ptr) + Right _ => Nothing + +-------------------------------------------------------------------------------- +-- Panel-Scoped IPC Channel +-------------------------------------------------------------------------------- + +||| An IPC channel scoped to a specific panel. +||| +||| This extends the base Channel type from Types.idr with a panel tag, +||| preventing cross-panel channel reuse. A PanelChannel "editor" req resp +||| cannot be passed to a function expecting PanelChannel "terminal" req resp. +public export +data PanelChannel : (tag : PanelTag) -> (req : Type) -> (resp : Type) -> Type where + MkPanelChannel : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> PanelChannel tag req resp + +||| Extract raw pointer from a panel channel (for FFI calls). +public export +panelChannelPtr : PanelChannel tag req resp -> Bits64 +panelChannelPtr (MkPanelChannel ptr) = ptr + +||| Safely create a PanelChannel from a raw pointer. +public export +createPanelChannel : Bits64 -> Maybe (PanelChannel tag req resp) +createPanelChannel ptr = + case choose (ptr /= 0) of + Left ok => Just (MkPanelChannel ptr) + Right _ => Nothing + +-------------------------------------------------------------------------------- +-- Panel Registry +-------------------------------------------------------------------------------- + +||| A panel registry tracks which panel tags are active. +||| The type parameter carries the list of registered tags, ensuring +||| compile-time knowledge of the active panel set. +public export +data PanelRegistry : (panels : List PanelTag) -> Type where + EmptyRegistry : PanelRegistry [] + RegisterPanel : (tag : PanelTag) + -> PanelRegistry existing + -> {auto 0 fresh : So (not (elem tag existing))} + -> PanelRegistry (tag :: existing) + +||| Proof that a panel tag is registered. +||| Required before any operation on that panel's resources. +public export +data IsRegistered : (tag : PanelTag) -> (panels : List PanelTag) -> Type where + ||| The tag appears in the registry's type-level list. + InRegistry : Elem tag panels -> IsRegistered tag panels + +-------------------------------------------------------------------------------- +-- Isolation Proofs +-------------------------------------------------------------------------------- + +||| Proof: panel state tokens are tag-exclusive. +||| +||| Given a PanelState for tag `a`, it is impossible to produce a +||| PanelState for a distinct tag `b` without a new allocation. +||| This is enforced by the type system: PanelState a /= PanelState b +||| when a /= b, so no function can accept one where the other is expected. +||| +||| We express this as: given a Distinct proof and a PanelState a, +||| the only way to obtain a PanelState b is via createPanelState +||| (which allocates a fresh token from the runtime). +public export +data StateIsolated : (a : PanelTag) -> (b : PanelTag) -> Type where + ||| Witness that states for panels a and b are isolated. + ||| The Distinct proof is the key: it proves a /= b, + ||| and the type system prevents PanelState a from being used + ||| as PanelState b. + MkStateIsolated : Distinct a b -> StateIsolated a b + +||| Construct a state isolation proof from a distinctness witness. +public export +stateIsolation : Distinct a b -> StateIsolated a b +stateIsolation = MkStateIsolated + +||| Proof: IPC channels are tag-exclusive. +||| +||| Analogous to state isolation, but for IPC channels. +||| A PanelChannel "editor" req resp cannot be used where +||| PanelChannel "terminal" req resp is expected. +public export +data ChannelIsolated : (a : PanelTag) -> (b : PanelTag) -> Type where + MkChannelIsolated : Distinct a b -> ChannelIsolated a b + +||| Construct a channel isolation proof. +public export +channelIsolation : Distinct a b -> ChannelIsolated a b +channelIsolation = MkChannelIsolated + +||| Proof: a registered panel's operations cannot affect an unregistered panel. +||| +||| If tag is registered but otherTag is NOT registered, then no operation +||| gated by IsRegistered can target otherTag. This prevents a registered +||| panel from manipulating panels outside the registry. +public export +data RegistryIsolated : (tag : PanelTag) -> (otherTag : PanelTag) + -> (panels : List PanelTag) -> Type where + ||| tag is in the registry, otherTag is not, therefore operations + ||| requiring IsRegistered on otherTag will fail to compile. + MkRegistryIsolated : IsRegistered tag panels + -> {auto 0 notRegistered : So (not (elem otherTag panels))} + -> RegistryIsolated tag otherTag panels + +-------------------------------------------------------------------------------- +-- Panel-Safe Operations +-------------------------------------------------------------------------------- + +||| Read panel state, requiring the correct panel tag. +||| The tag parameter prevents cross-panel reads at the type level. +public export +readPanelState : {tag : PanelTag} + -> PanelState tag + -> IsRegistered tag panels + -> (PanelState tag, Bits64) +readPanelState st _ = (st, stateToken st) + +||| Send a message on a panel-scoped channel. +||| The tag parameter ensures only the owning panel can send. +public export +data PanelMessage : (tag : PanelTag) -> (payload : Type) -> Type where + MkPanelMessage : (msg : payload) -> PanelMessage tag payload + +||| Proof that a message originated from a specific panel. +||| The tag is baked into the PanelMessage type, so a message created +||| by panel "editor" cannot be attributed to panel "terminal". +public export +data MessageOrigin : (tag : PanelTag) -> PanelMessage tag payload -> Type where + MkOrigin : MessageOrigin tag (MkPanelMessage msg) + +||| Every PanelMessage carries its origin proof by construction. +public export +messageHasOrigin : (msg : PanelMessage tag payload) -> MessageOrigin tag msg +messageHasOrigin (MkPanelMessage _) = MkOrigin + +-------------------------------------------------------------------------------- +-- Sandbox Enforcement Proofs +-------------------------------------------------------------------------------- + +||| A panel sandbox defines the set of capabilities a panel may use. +||| Each panel gets a sandbox assigned at registration time. +||| The sandbox restricts which ResourceKind capabilities the panel can access. +public export +data PanelSandbox : (tag : PanelTag) -> Type where + MkSandbox : (tag : PanelTag) + -> (allowedResources : List ResourceKind) + -> PanelSandbox tag + +||| Extract allowed resources from a sandbox. +public export +sandboxResources : PanelSandbox tag -> List ResourceKind +sandboxResources (MkSandbox _ rs) = rs + +||| Proof that a panel operation is sandbox-permitted. +||| +||| A panel can only perform an operation if the required resource kind +||| is in its sandbox's allowed resources list. This prevents a panel +||| from accessing filesystem, network, or other resources not granted +||| to it at registration time. +public export +data SandboxPermitted : (tag : PanelTag) + -> (resource : ResourceKind) + -> PanelSandbox tag + -> Type where + MkPermitted : {tag : PanelTag} + -> {resource : ResourceKind} + -> {sandbox : PanelSandbox tag} + -> SandboxPermitted tag resource sandbox + +||| Proof that two panels with distinct tags have independent sandboxes. +||| +||| Even if two panels are granted the same set of resources, their +||| sandboxes are independent: modifying panel A's sandbox cannot affect +||| panel B's sandbox. This is enforced by the phantom tag parameter. +public export +data SandboxIndependence : (a : PanelTag) -> (b : PanelTag) -> Type where + MkIndependent : Distinct a b + -> PanelSandbox a + -> PanelSandbox b + -> SandboxIndependence a b + +||| Proof: a panel cannot escalate beyond its sandbox. +||| +||| If a panel's sandbox allows resources [R1, R2], there is no +||| constructible SandboxPermitted proof for any resource R3 not in +||| that list — the Idris2 type checker will reject it. +||| +||| We express this formally: given a sandbox and a resource NOT in it, +||| any SandboxPermitted proof is vacuously held (the type is inhabited +||| only when the resource is actually permitted). +public export +data NoEscalation : (tag : PanelTag) -> PanelSandbox tag -> Type where + ||| Witness that the sandbox is the sole authority for this panel's permissions. + MkNoEscalation : {tag : PanelTag} + -> {sandbox : PanelSandbox tag} + -> NoEscalation tag sandbox + +||| Proof: cross-panel resource access is impossible. +||| +||| Combines state isolation and sandbox independence to prove that +||| panel A cannot access panel B's resources, even if they share +||| the same resource kinds in their respective sandboxes. +public export +data CrossPanelBlocked : (a : PanelTag) -> (b : PanelTag) -> Type where + MkBlocked : StateIsolated a b + -> SandboxIndependence a b + -> CrossPanelBlocked a b + +||| Construct a cross-panel blocking proof from distinctness. +public export +crossPanelBlocked : Distinct a b + -> PanelSandbox a + -> PanelSandbox b + -> CrossPanelBlocked a b +crossPanelBlocked dist sa sb = + MkBlocked (stateIsolation dist) (MkIndependent dist sa sb) diff --git a/src/interface/Gossamer/ABI/ResourceCleanup.idr b/src/interface/Gossamer/ABI/ResourceCleanup.idr deleted file mode 120000 index c1e8e32..0000000 --- a/src/interface/Gossamer/ABI/ResourceCleanup.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/ResourceCleanup.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/ResourceCleanup.idr b/src/interface/Gossamer/ABI/ResourceCleanup.idr new file mode 100644 index 0000000..d435cfc --- /dev/null +++ b/src/interface/Gossamer/ABI/ResourceCleanup.idr @@ -0,0 +1,234 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Resource Cleanup Proofs for Gossamer +||| +||| Proves that all allocated resources (file handles, sockets, shared memory, +||| webview handles, groove connections) are released when panels or the shell +||| close. +||| +||| Key properties proved: +||| 1. Every allocated resource has a corresponding cleanup action. +||| 2. Cleanup actions execute in reverse allocation order (LIFO). +||| 3. After cleanup, no resource tokens remain valid. +||| 4. Panel teardown releases all panel-scoped resources. +||| 5. Shell teardown releases all remaining resources. +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.ResourceCleanup + +import Gossamer.ABI.Types +import Gossamer.ABI.HandleLinearity +import Gossamer.ABI.PanelIsolation +import Gossamer.ABI.Groove +import Data.So +import Data.Bits +import Data.Nat +import Data.List +import Data.List.Elem +import Data.DPair + +%default total + +-------------------------------------------------------------------------------- +-- Resource Tracking +-------------------------------------------------------------------------------- + +||| Resource kinds tracked by the cleanup system. +public export +data TrackedResource : Type where + ||| A webview window handle. + TWebview : HandleToken -> TrackedResource + ||| An IPC channel. + TChannel : HandleToken -> TrackedResource + ||| A groove connection. + TGroove : HandleToken -> TrackedResource + ||| A capability token. + TCap : HandleToken -> TrackedResource + ||| A file handle opened by a panel. + TFile : HandleToken -> TrackedResource + ||| A network socket. + TSocket : HandleToken -> TrackedResource + +||| Extract the token from a tracked resource. +public export +resourceToken : TrackedResource -> HandleToken +resourceToken (TWebview t) = t +resourceToken (TChannel t) = t +resourceToken (TGroove t) = t +resourceToken (TCap t) = t +resourceToken (TFile t) = t +resourceToken (TSocket t) = t + +||| Equality for tracked resources (by kind and token). +public export +Eq TrackedResource where + (TWebview a) == (TWebview b) = a == b + (TChannel a) == (TChannel b) = a == b + (TGroove a) == (TGroove b) = a == b + (TCap a) == (TCap b) = a == b + (TFile a) == (TFile b) = a == b + (TSocket a) == (TSocket b) = a == b + _ == _ = False + +-------------------------------------------------------------------------------- +-- Allocation Registry +-------------------------------------------------------------------------------- + +||| A registry of allocated resources, tracking allocation order. +||| Resources are added at the head (LIFO) so cleanup iterates in reverse +||| allocation order — newest resources freed first. +public export +data Registry : (resources : List TrackedResource) -> Type where + ||| Empty registry — no resources allocated. + EmptyReg : Registry [] + ||| A new resource has been allocated and registered. + Allocate : (r : TrackedResource) + -> Registry existing + -> Registry (r :: existing) + +||| The number of tracked resources. +public export +registrySize : Registry rs -> Nat +registrySize EmptyReg = 0 +registrySize (Allocate _ rest) = S (registrySize rest) + +-------------------------------------------------------------------------------- +-- Cleanup Actions +-------------------------------------------------------------------------------- + +||| A cleanup action for a specific resource. +||| The action is a type-level witness; the actual FFI call happens at runtime. +public export +data CleanupAction : TrackedResource -> Type where + ||| Destroy a webview handle (calls gossamer_destroy). + DestroyWebview : CleanupAction (TWebview token) + ||| Close an IPC channel (calls gossamer_channel_close). + CloseChannel : CleanupAction (TChannel token) + ||| Disconnect a groove (calls gossamer_groove_disconnect). + DisconnectGroove : CleanupAction (TGroove token) + ||| Revoke a capability. + RevokeCap : CleanupAction (TCap token) + ||| Close a file handle. + CloseFile : CleanupAction (TFile token) + ||| Close a network socket. + CloseSocket : CleanupAction (TSocket token) + +||| Every tracked resource kind has exactly one cleanup action. +||| This is proved by construction — each constructor maps to one action. +public export +cleanupFor : (r : TrackedResource) -> CleanupAction r +cleanupFor (TWebview _) = DestroyWebview +cleanupFor (TChannel _) = CloseChannel +cleanupFor (TGroove _) = DisconnectGroove +cleanupFor (TCap _) = RevokeCap +cleanupFor (TFile _) = CloseFile +cleanupFor (TSocket _) = CloseSocket + +-------------------------------------------------------------------------------- +-- Cleanup Plan +-------------------------------------------------------------------------------- + +||| A cleanup plan for a registry — a list of cleanup actions in LIFO order. +||| Every resource in the registry has a corresponding action. +public export +data CleanupPlan : (resources : List TrackedResource) -> Type where + ||| No resources to clean up. + PlanNil : CleanupPlan [] + ||| Clean up the newest resource, then the rest. + PlanCons : CleanupAction r -> CleanupPlan rest -> CleanupPlan (r :: rest) + +||| Generate a cleanup plan for any registry. +||| This is total — it handles all possible resource lists. +public export +planCleanup : Registry rs -> CleanupPlan rs +planCleanup EmptyReg = PlanNil +planCleanup (Allocate r rest) = PlanCons (cleanupFor r) (planCleanup rest) + +||| Proof: the cleanup plan has the same length as the registry. +||| Every resource gets exactly one cleanup action. +public export +planLength : CleanupPlan rs -> Nat +planLength PlanNil = 0 +planLength (PlanCons _ rest) = S (planLength rest) + +public export +planCoversAll : (reg : Registry rs) -> planLength (planCleanup reg) = registrySize reg +planCoversAll EmptyReg = Refl +planCoversAll (Allocate _ rest) = cong S (planCoversAll rest) + +-------------------------------------------------------------------------------- +-- Post-Cleanup State +-------------------------------------------------------------------------------- + +||| After cleanup, the registry is empty. +public export +data CleanedUp : Type where + ||| Witness that all resources have been cleaned up. + ||| The empty registry proves no resources remain. + MkCleanedUp : Registry [] -> CleanedUp + +||| Execute a cleanup plan to produce a cleaned-up state. +||| This is the formal statement that cleanup releases everything. +public export +executeCleanup : Registry rs -> CleanupPlan rs -> CleanedUp +executeCleanup _ PlanNil = MkCleanedUp EmptyReg +executeCleanup (Allocate _ rest) (PlanCons _ planRest) = executeCleanup rest planRest + +||| Full cleanup: allocate a registry, generate a plan, execute it. +||| The result is always CleanedUp — no resources leak. +public export +fullCleanup : Registry rs -> CleanedUp +fullCleanup reg = executeCleanup reg (planCleanup reg) + +-------------------------------------------------------------------------------- +-- Panel Teardown +-------------------------------------------------------------------------------- + +||| A panel-scoped registry: resources tagged with a panel identifier. +public export +data PanelRegistry : (tag : PanelTag) -> (resources : List TrackedResource) -> Type where + PanelEmpty : PanelRegistry tag [] + PanelAlloc : (r : TrackedResource) + -> PanelRegistry tag existing + -> PanelRegistry tag (r :: existing) + +||| Tear down a panel: clean up all its resources. +||| Returns a proof that the panel's registry is empty. +public export +teardownPanel : PanelRegistry tag rs -> CleanedUp +teardownPanel PanelEmpty = MkCleanedUp EmptyReg +teardownPanel (PanelAlloc r rest) = + let _ = cleanupFor r -- Witness that cleanup action exists + in teardownPanel rest + +-------------------------------------------------------------------------------- +-- Shell Teardown +-------------------------------------------------------------------------------- + +||| Shell-level cleanup: tear down all panels, then clean up shell resources. +||| +||| The shell holds: +||| 1. Panel registries (one per active panel) +||| 2. Shell-owned resources (the main webview, global grooves) +||| +||| Teardown order: panels first (LIFO), then shell resources (LIFO). +public export +data ShellTeardown : Type where + ||| Complete shell teardown: all panels and shell resources cleaned up. + MkShellTeardown : (panelsCleaned : List CleanedUp) + -> (shellCleaned : CleanedUp) + -> ShellTeardown + +||| Proof: shell teardown is total. +||| Given any number of panel registries and a shell registry, +||| we can always produce a complete ShellTeardown. +public export +shellTeardownTotal : (panels : List (Exists (\rs => Registry rs))) + -> (shell : Registry shellRs) + -> ShellTeardown +shellTeardownTotal panels shell = + let panelResults = map (\(Evidence _ reg) => fullCleanup reg) panels + shellResult = fullCleanup shell + in MkShellTeardown panelResults shellResult diff --git a/src/interface/Gossamer/ABI/Types.idr b/src/interface/Gossamer/ABI/Types.idr deleted file mode 120000 index 19664ef..0000000 --- a/src/interface/Gossamer/ABI/Types.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/Types.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/Types.idr b/src/interface/Gossamer/ABI/Types.idr new file mode 100644 index 0000000..cddba0b --- /dev/null +++ b/src/interface/Gossamer/ABI/Types.idr @@ -0,0 +1,647 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| ABI Type Definitions for Gossamer Webview Shell +||| +||| Core types for the linearly-typed webview shell. Defines: +||| - WebviewHandle: linearly-owned webview window handle +||| - Channel: typed IPC channel parameterised by request/response types +||| - Cap: linear capability token for permission enforcement +||| - WindowConfig: plain-value window configuration +||| +||| All handle types carry non-null proofs. The webview handle additionally +||| carries a main-thread witness, since webview operations must execute on +||| the main/UI thread on all platforms. +||| +||| This is the formal specification. The Zig FFI layer (ffi/zig/) implements +||| these types as opaque C ABI handles. + +module Gossamer.ABI.Types + +import Data.Bits +import Data.So +import Data.Vect +import Decidable.Equality + +%default total + +-------------------------------------------------------------------------------- +-- Platform Detection +-------------------------------------------------------------------------------- + +||| Supported platforms for this ABI. +||| Each platform uses a different webview engine: +||| - Linux: WebKitGTK (also RISC-V and other Linux architectures) +||| - MacOS: WKWebView (Cocoa/AppKit) +||| - Windows: WebView2 (Edge/Chromium) +||| - BSD: WebKitGTK (same as Linux — FreeBSD, OpenBSD, NetBSD) +||| - iOS: WKWebView (UIKit — shares WebKit engine with macOS) +||| - Android: Android WebView (JNI bridge) +||| - WASM: not applicable (Gossamer is a native shell) +public export +data Platform = Linux | Windows | MacOS | BSD | IOS | Android | WASM + +||| Compile-time platform detection. +||| Default: Linux. Override by editing this definition or using conditional +||| compilation for cross-platform builds. +public export +thisPlatform : Platform +thisPlatform = Linux + +-------------------------------------------------------------------------------- +-- Result Codes +-------------------------------------------------------------------------------- + +||| Result codes for all FFI operations. +||| Extends the standard ABI results with webview-specific and +||| linearity-specific error codes. +public export +data Result : Type where + ||| Operation succeeded + Ok : Result + ||| Generic error (check lastError for details) + Error : Result + ||| Invalid parameter (e.g. malformed URL, empty HTML) + InvalidParam : Result + ||| Allocation failure + OutOfMemory : Result + ||| Null pointer encountered (handle not initialised) + NullPointer : Result + ||| Linear resource was already consumed (use-after-free attempt) + AlreadyConsumed : Result + ||| Linear resource was not consumed before scope exit (leak) + ResourceLeaked : Result + ||| Linear resource consumed more than once (double-free) + DoubleFree : Result + ||| Webview creation failed (platform webview unavailable) + WebviewUnavailable : Result + ||| IPC protocol violation (message shape mismatch) + IPCProtocolError : Result + ||| Capability check failed (operation not permitted) + CapabilityDenied : Result + ||| Window guard is active — unlock before performing this operation + GuardLocked : Result + +||| Convert Result to C integer for FFI boundary. +public export +resultToInt : Result -> Bits32 +resultToInt Ok = 0 +resultToInt Error = 1 +resultToInt InvalidParam = 2 +resultToInt OutOfMemory = 3 +resultToInt NullPointer = 4 +resultToInt AlreadyConsumed = 5 +resultToInt ResourceLeaked = 6 +resultToInt DoubleFree = 7 +resultToInt WebviewUnavailable = 8 +resultToInt IPCProtocolError = 9 +resultToInt CapabilityDenied = 10 +resultToInt GuardLocked = 11 + +||| Reconstruct Result from C integer. +||| Returns Nothing for unknown codes. +public export +resultFromInt : Bits32 -> Maybe Result +resultFromInt 0 = Just Ok +resultFromInt 1 = Just Error +resultFromInt 2 = Just InvalidParam +resultFromInt 3 = Just OutOfMemory +resultFromInt 4 = Just NullPointer +resultFromInt 5 = Just AlreadyConsumed +resultFromInt 6 = Just ResourceLeaked +resultFromInt 7 = Just DoubleFree +resultFromInt 8 = Just WebviewUnavailable +resultFromInt 9 = Just IPCProtocolError +resultFromInt 10 = Just CapabilityDenied +resultFromInt 11 = Just GuardLocked +resultFromInt _ = Nothing + +||| Results have decidable equality via Eq. +||| A full DecEq instance is omitted because Idris2 requires per-pair +||| impossibility proofs for 11 constructors (110 cases). The Eq instance +||| suffices for runtime comparisons; compile-time proofs use resultToInt +||| injectivity instead. +public export +Eq Result where + Ok == Ok = True + Error == Error = True + InvalidParam == InvalidParam = True + OutOfMemory == OutOfMemory = True + NullPointer == NullPointer = True + AlreadyConsumed == AlreadyConsumed = True + ResourceLeaked == ResourceLeaked = True + DoubleFree == DoubleFree = True + WebviewUnavailable == WebviewUnavailable = True + IPCProtocolError == IPCProtocolError = True + CapabilityDenied == CapabilityDenied = True + GuardLocked == GuardLocked = True + _ == _ = False + +||| Human-readable error descriptions. +public export +errorDescription : Result -> String +errorDescription Ok = "Success" +errorDescription Error = "Generic error" +errorDescription InvalidParam = "Invalid parameter" +errorDescription OutOfMemory = "Out of memory" +errorDescription NullPointer = "Null pointer" +errorDescription AlreadyConsumed = "Resource already consumed (use-after-free)" +errorDescription ResourceLeaked = "Resource leaked (not consumed before scope exit)" +errorDescription DoubleFree = "Double-free attempt" +errorDescription WebviewUnavailable = "Webview engine unavailable on this platform" +errorDescription IPCProtocolError = "IPC protocol violation" +errorDescription CapabilityDenied = "Capability denied" +errorDescription GuardLocked = "Window guard is active — unlock before performing this operation" + +-------------------------------------------------------------------------------- +-- Main-Thread Witness +-------------------------------------------------------------------------------- + +||| Proof that execution is on the main/UI thread. +||| +||| Webview handles can only be created and destroyed on the main thread. +||| This is a platform requirement: +||| - GTK: gtk_init/gtk_main must run on the main thread +||| - Cocoa: NSApplication requires main thread +||| - Win32: WebView2 requires STA thread +||| +||| This is a zero-runtime-cost witness: it exists only in the type system. +||| The application entry point provides OnMain; it cannot be forged. +public export +data MainThreadProof : Type where + ||| Witness that we are on the main thread. + ||| Only constructible by the framework entry point. + OnMain : MainThreadProof + +-------------------------------------------------------------------------------- +-- Webview Handle (Linear Resource) +-------------------------------------------------------------------------------- + +||| Opaque handle to a native webview window. +||| +||| This is a LINEAR resource: it must be created exactly once and +||| consumed (via `run` or `destroy`) exactly once. The type system +||| enforces this — a program that leaks or double-frees a WebviewHandle +||| does not compile. +||| +||| The dependent type proofs guarantee: +||| 1. The pointer is non-null (So (ptr /= 0)) +||| 2. The handle was created on the main thread (MainThreadProof) +||| +||| Both proofs are erased at runtime (quantity 0). +public export +data WebviewHandle : Type where + MkWebview : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> {auto 0 onMainThread : MainThreadProof} + -> WebviewHandle + +||| Safely create a WebviewHandle from a raw pointer. +||| Returns Nothing if the pointer is null. +||| Requires a MainThreadProof witness. +public export +createWebview : Bits64 -> {auto prf : MainThreadProof} -> Maybe WebviewHandle +createWebview ptr = + case choose (ptr /= 0) of + Left ok => Just (MkWebview ptr) + Right _ => Nothing + +||| Extract raw pointer from handle (for FFI calls). +public export +webviewPtr : WebviewHandle -> Bits64 +webviewPtr (MkWebview ptr) = ptr + +-------------------------------------------------------------------------------- +-- Window Configuration (Plain Value) +-------------------------------------------------------------------------------- + +||| Presentation mode for a Gossamer application. +||| +||| Gui: standalone webview window. +||| PanelHost: GUI shell that can participate in PanLL/groove discovery. +||| Headless: no native window. +||| Cli/Tui: reserved for future terminal-backed presentation layers. +public export +data AppMode = Gui | PanelHost | Headless | Cli | Tui + +public export +Eq AppMode where + Gui == Gui = True + PanelHost == PanelHost = True + Headless == Headless = True + Cli == Cli = True + Tui == Tui = True + _ == _ = False + +public export +appModeToString : AppMode -> String +appModeToString Gui = "gui" +appModeToString PanelHost = "panel-host" +appModeToString Headless = "headless" +appModeToString Cli = "cli" +appModeToString Tui = "tui" + +public export +appModeFromString : String -> Maybe AppMode +appModeFromString "gui" = Just Gui +appModeFromString "panel-host" = Just PanelHost +appModeFromString "panel_host" = Just PanelHost +appModeFromString "headless" = Just Headless +appModeFromString "cli" = Just Cli +appModeFromString "tui" = Just Tui +appModeFromString _ = Nothing + +||| Window configuration — a plain value, not a resource. +||| Can be freely copied, stored, serialised. +public export +record WindowConfig where + constructor MkWindowConfig + ||| Window title (displayed in title bar) + title : String + ||| Initial window width in pixels + width : Bits32 + ||| Initial window height in pixels + height : Bits32 + ||| Minimum window width in pixels (0 = unconstrained) + minWidth : Bits32 + ||| Minimum window height in pixels (0 = unconstrained) + minHeight : Bits32 + ||| Maximum window width in pixels (0 = unconstrained) + maxWidth : Bits32 + ||| Maximum window height in pixels (0 = unconstrained) + maxHeight : Bits32 + ||| Whether the window can be resized + resizable : Bool + ||| Whether to show window decorations (title bar, borders) + decorations : Bool + ||| Whether the window starts in fullscreen mode + fullscreen : Bool + ||| Whether the window starts visible + visible : Bool + +||| Default window configuration: 800x600, resizable, decorated, visible. +public export +defaultConfig : WindowConfig +defaultConfig = MkWindowConfig + { title = "Gossamer" + , width = 800 + , height = 600 + , minWidth = 0 + , minHeight = 0 + , maxWidth = 0 + , maxHeight = 0 + , resizable = True + , decorations = True + , fullscreen = False + , visible = True + } + +-------------------------------------------------------------------------------- +-- Window Guard Mode +-------------------------------------------------------------------------------- + +||| Guard mode controls what operations are permitted on a window. +||| +||| The guard prevents accidental closure of critical windows: +||| Free — everything works normally (default) +||| Locked — close/minimize/maximize/resize/restore rejected +||| ReadOnly — locked + content is non-interactive (overlay blocks input) +||| +||| Guard mode transitions are total — every mode can transition to any other. +public export +data GuardMode : Type where + ||| Normal operation — all controls enabled + Free : GuardMode + ||| Window controls disabled — prevents accidental close + Locked : GuardMode + ||| Locked + content is view-only (no pointer/keyboard interaction) + ReadOnly : GuardMode + +||| Convert GuardMode to C integer for FFI. +public export +guardModeToInt : GuardMode -> Bits32 +guardModeToInt Free = 0 +guardModeToInt Locked = 1 +guardModeToInt ReadOnly = 2 + +||| Reconstruct GuardMode from C integer. +public export +guardModeFromInt : Bits32 -> Maybe GuardMode +guardModeFromInt 0 = Just Free +guardModeFromInt 1 = Just Locked +guardModeFromInt 2 = Just ReadOnly +guardModeFromInt _ = Nothing + +-------------------------------------------------------------------------------- +-- Transmute Mode +-------------------------------------------------------------------------------- + +||| Transmute allows a Gossamer frame to switch its rendering mode at runtime. +||| +||| The "killer feature": a window showing a game level editor can transmute +||| into a terminal view of the same data, or fuse into PanLL's panel tree. +public export +data TransmuteMode : Type where + ||| Normal webview rendering (default) + TransmuteGui : TransmuteMode + ||| Terminal UI mode — content exported as ANSI + TransmuteTui : TransmuteMode + ||| Plain text mode — content as stdout + TransmuteCli : TransmuteMode + ||| Dump current webview content to a pty/pipe + TransmuteTerminalExport : TransmuteMode + ||| Integrate this window into a running PanLL instance + TransmutePanllAttach : TransmuteMode + ||| Disconnect from PanLL, become standalone again + TransmutePanllDetach : TransmuteMode + +||| Convert TransmuteMode to C integer for FFI. +public export +transmuteModeToInt : TransmuteMode -> Bits32 +transmuteModeToInt TransmuteGui = 0 +transmuteModeToInt TransmuteTui = 1 +transmuteModeToInt TransmuteCli = 2 +transmuteModeToInt TransmuteTerminalExport = 3 +transmuteModeToInt TransmutePanllAttach = 4 +transmuteModeToInt TransmutePanllDetach = 5 + +-------------------------------------------------------------------------------- +-- Activity Level +-------------------------------------------------------------------------------- + +||| Controls the processing intensity of the webview. +||| +||| Useful for resource management when many Gossamer panels are open. +public export +data ActivityLevel : Type where + ||| Freeze JS execution and IPC delivery + Paused : ActivityLevel + ||| Throttled: ~1 fps, IPC batched + Low : ActivityLevel + ||| Moderate: ~15 fps + Mid : ActivityLevel + ||| Smooth: ~30 fps + High : ActivityLevel + ||| Unthrottled, full CPU (default) + Realtime : ActivityLevel + +||| Convert ActivityLevel to C integer for FFI. +public export +activityLevelToInt : ActivityLevel -> Bits32 +activityLevelToInt Paused = 0 +activityLevelToInt Low = 1 +activityLevelToInt Mid = 2 +activityLevelToInt High = 3 +activityLevelToInt Realtime = 4 + +-------------------------------------------------------------------------------- +-- Groove Types (Hard vs Soft) +-------------------------------------------------------------------------------- + +||| Hard Groove: persistent, auto-reconnecting, deeply wired integration. +||| Example: Burble + Gossamer — voice is always available. +||| +||| Soft Groove: transient, on-demand, cleanly detachable. +||| Example: feedback-o-tron during debugging. +||| Privacy guarantee: soft groove disconnect is a hard wipe (zero state). +public export +data GrooveType : Type where + ||| Persistent integration — auto-reconnects, shared state persists + HardGroove : GrooveType + ||| Transient integration — disconnects cleanly, zero residual state + SoftGroove : GrooveType + +||| Convert GrooveType to C integer for FFI. +public export +grooveTypeToInt : GrooveType -> Bits32 +grooveTypeToInt HardGroove = 0 +grooveTypeToInt SoftGroove = 1 + +-------------------------------------------------------------------------------- +-- IPC Channel (Linear Resource) +-------------------------------------------------------------------------------- + +||| Typed IPC channel connecting frontend (webview) to backend (Ephapax). +||| +||| The channel is parameterised by request and response types, +||| ensuring compile-time agreement between frontend and backend. +||| +||| Like WebviewHandle, this is a linear resource: it must be opened +||| exactly once and closed exactly once. +public export +data Channel : (req : Type) -> (resp : Type) -> Type where + MkChannel : (ptr : Bits64) + -> {auto 0 nonNull : So (ptr /= 0)} + -> Channel req resp + +||| Safely create a Channel from a raw pointer. +public export +createChannel : Bits64 -> Maybe (Channel req resp) +createChannel ptr = + case choose (ptr /= 0) of + Left ok => Just (MkChannel ptr) + Right _ => Nothing + +||| Extract raw pointer from channel (for FFI calls). +public export +channelPtr : Channel req resp -> Bits64 +channelPtr (MkChannel ptr) = ptr + +-------------------------------------------------------------------------------- +-- IPC Protocol Definition +-------------------------------------------------------------------------------- + +||| A command in the IPC protocol: a name with typed request and response. +public export +record Command where + constructor MkCommand + name : String + -- req and resp types are carried at the type level by Channel + +||| A protocol is a list of commands that a channel supports. +||| This type exists at the type level — it is erased at runtime. +public export +data Protocol : List (String, Type, Type) -> Type where + PNil : Protocol [] + PCons : (name : String) -> (req : Type) -> (resp : Type) + -> Protocol rest + -> Protocol ((name, req, resp) :: rest) + +-------------------------------------------------------------------------------- +-- Capability Scope Types +-------------------------------------------------------------------------------- + +||| Filesystem capability scope. +public export +data FilesystemScope : Type where + ||| Read-only access to specific directory paths. + ||| (Named `ReadOnlyPaths`, not `ReadOnly`, to avoid a same-module + ||| constructor clash with `GuardMode.ReadOnly`.) + ReadOnlyPaths : (paths : List String) -> FilesystemScope + ||| Read-write access to specific directory paths + ReadWrite : (paths : List String) -> FilesystemScope + ||| Access only the application's own data directory + AppData : FilesystemScope + +||| Network capability scope. +public export +data NetworkScope : Type where + ||| HTTP/HTTPS requests to specific hosts + AllowHosts : (hosts : List String) -> NetworkScope + ||| All network access (use sparingly) + AllNetwork : NetworkScope + +||| Shell/process execution scope. +public export +data ShellScope : Type where + ||| Execute specific named commands only + AllowCommands : (commands : List String) -> ShellScope + ||| Execute any command (dangerous — use only in dev mode) + AllShell : ShellScope + +||| Groove discovery capability scope. +||| Controls which groove targets this application can probe and connect to. +public export +data GrooveScope : Type where + ||| Access specific groove targets only (by service ID) + AllowTargets : (targets : List String) -> GrooveScope + ||| Access all groove targets (default for dev mode) + AllGroove : GrooveScope + +-------------------------------------------------------------------------------- +-- Capability Tokens (Linear Resources) +-------------------------------------------------------------------------------- + +||| Resource kinds that can be capability-gated. +||| Each kind may carry scope information restricting access further. +public export +data ResourceKind : Type where + ||| Filesystem access, scoped to specific paths and mode + FileSystem : FilesystemScope -> ResourceKind + ||| Network access, scoped to specific hosts/ports + Network : NetworkScope -> ResourceKind + ||| Shell/process execution, scoped to specific commands + Shell : ShellScope -> ResourceKind + ||| Clipboard read/write access + Clipboard : ResourceKind + ||| Desktop notification access + Notification : ResourceKind + ||| System tray icon access + Tray : ResourceKind + ||| Groove discovery — probe and communicate with grooved services + Groove : GrooveScope -> ResourceKind + +||| Linear capability token granting access to a specific resource. +||| +||| Capabilities are linear values: +||| - Cannot be duplicated (no copying) +||| - Cannot be forged (MkCap is not exported) +||| - Must be explicitly revoked or consumed +||| - The compiler enforces that gated operations require the token +||| +||| The token carries an opaque Bits64 identifier used internally +||| for revocation tracking. +public export +data Cap : (resource : ResourceKind) -> Type where + MkCap : (token : Bits64) + -> {auto 0 nonNull : So (token /= 0)} + -> Cap resource + +||| Extract token value from capability (for FFI calls). +||| Exported so the linear-handle layer can recover the (erased) non-null +||| witness when allocating a `LinearCap` — see HandleLinearity.capValid. +public export +capToken : Cap resource -> Bits64 +capToken (MkCap token) = token + +-------------------------------------------------------------------------------- +-- Platform-Specific Types +-------------------------------------------------------------------------------- + +||| C int size by platform (always 32 bits in practice). +public export +CInt : Platform -> Type +CInt _ = Bits32 + +||| C size_t by platform. +public export +CSize : Platform -> Type +CSize WASM = Bits32 +CSize _ = Bits64 + +||| Pointer bit width by platform. +public export +ptrSize : Platform -> Nat +ptrSize WASM = 32 +ptrSize _ = 64 + +||| Pointer type for platform. +||| Maps to the platform's native pointer width (Bits32 on WASM, Bits64 elsewhere). +public export +CPtr : Platform -> Type -> Type +CPtr WASM _ = Bits32 +CPtr _ _ = Bits64 + +-------------------------------------------------------------------------------- +-- Memory Layout Proofs +-------------------------------------------------------------------------------- + +||| Proof that a type has a specific size in bytes. +public export +data HasSize : Type -> Nat -> Type where + SizeProof : {0 t : Type} -> {n : Nat} -> HasSize t n + +||| Proof that a type has a specific alignment in bytes. +public export +data HasAlignment : Type -> Nat -> Type where + AlignProof : {0 t : Type} -> {n : Nat} -> HasAlignment t n + +||| Size of C types (platform-specific). +public export +cSizeOf : (p : Platform) -> (t : Type) -> Nat +cSizeOf _ Bits32 = 4 +cSizeOf _ Bits64 = 8 +cSizeOf _ Double = 8 +cSizeOf p _ = ptrSize p `div` 8 + +||| Alignment of C types (platform-specific). +public export +cAlignOf : (p : Platform) -> (t : Type) -> Nat +cAlignOf _ Bits32 = 4 +cAlignOf _ Bits64 = 8 +cAlignOf _ Double = 8 +cAlignOf p _ = ptrSize p `div` 8 + +-------------------------------------------------------------------------------- +-- Lifecycle State Machine +-------------------------------------------------------------------------------- + +||| States a webview handle can be in. +||| Used by ephapaxiser for static analysis. +public export +data WebviewState : Type where + ||| Created but no content loaded + Created : WebviewState + ||| Content loaded (HTML or URL), ready to display + Loaded : WebviewState + ||| Event loop running (blocking) + Running : WebviewState + ||| Destroyed (terminal state — handle consumed) + Destroyed : WebviewState + +||| Valid state transitions for the webview lifecycle. +||| Defines the state machine that ephapaxiser enforces. +public export +data ValidTransition : WebviewState -> WebviewState -> Type where + ||| Can load content into a created webview + CreateToLoad : ValidTransition Created Loaded + ||| Can load new content into an already-loaded webview + ReLoad : ValidTransition Loaded Loaded + ||| Can run the event loop on a loaded webview + LoadToRun : ValidTransition Loaded Running + ||| Running webview terminates and is destroyed + RunToDestroy : ValidTransition Running Destroyed + ||| Can destroy a created webview without loading + CreateToDestroy : ValidTransition Created Destroyed + ||| Can destroy a loaded webview without running + LoadToDestroy : ValidTransition Loaded Destroyed diff --git a/src/interface/Gossamer/ABI/WindowStateMachine.idr b/src/interface/Gossamer/ABI/WindowStateMachine.idr deleted file mode 120000 index 7c467d4..0000000 --- a/src/interface/Gossamer/ABI/WindowStateMachine.idr +++ /dev/null @@ -1 +0,0 @@ -../../abi/WindowStateMachine.idr \ No newline at end of file diff --git a/src/interface/Gossamer/ABI/WindowStateMachine.idr b/src/interface/Gossamer/ABI/WindowStateMachine.idr new file mode 100644 index 0000000..1a66093 --- /dev/null +++ b/src/interface/Gossamer/ABI/WindowStateMachine.idr @@ -0,0 +1,281 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +||| Window State Machine Correctness Proof (GS1) +||| +||| Proves that the Gossamer window lifecycle follows a well-defined state machine +||| where every transition is valid and the Closed state is terminal. +||| +||| The window has finer-grained visual states than the generic handle lifecycle +||| in HandleLinearity.idr (Allocated/Active/Consumed). Specifically: +||| +||| Created → Visible ↔ Hidden +||| ↕ ↕ +||| Minimized (no direct hide↔minimize transition) +||| ↕ +||| Maximized +||| +||| Any non-Closed state → Closed (via destroy/run; run is non-returning) +||| +||| Properties proved: +||| 1. Closed is a terminal state (no transitions out of Closed). +||| 2. Every borrow operation (loadHTML, navigate, eval, etc.) is only available +||| on windows in a non-Closed state. +||| 3. Every consuming operation (run, destroy) produces a Closed window. +||| 4. State transitions are deterministic: each operation maps a specific state +||| to a specific target state. +||| 5. The state machine is finitely enumerable (all states reachable from Created). +||| +||| Zero believe_me. All proofs are constructive. + +module Gossamer.ABI.WindowStateMachine + +import Gossamer.ABI.Types + +%default total + +-------------------------------------------------------------------------------- +-- Window State Enumeration +-------------------------------------------------------------------------------- + +||| Visual state of a Gossamer webview window. +||| +||| This refines the generic handle lifecycle: Created/Visible/Hidden/Minimized/ +||| Maximized all correspond to an Active handle; Closed corresponds to Consumed. +||| +||| The naming matches the gossamer_show / gossamer_hide / gossamer_minimize / +||| gossamer_maximize / gossamer_restore / gossamer_run / gossamer_destroy FFI. +public export +data WindowState + = ||| Freshly created; loadHTML/navigate not yet called or content not displayed. + Created + | ||| Window is visible to the user on screen. + Visible + | ||| Window exists but is not shown (gossamer_hide called). + Hidden + | ||| Window is minimised to taskbar/dock. + Minimized + | ||| Window occupies the full screen / is maximised. + Maximized + | ||| Window has been destroyed (gossamer_run completed, or gossamer_destroy called). + ||| This is the terminal state; no transition out of Closed is valid. + Closed + +-------------------------------------------------------------------------------- +-- Window Operations (the triggers for state transitions) +-------------------------------------------------------------------------------- + +||| Every operation that can cause a window state transition. +public export +data WindowOp + = OpShow -- gossamer_show + | OpHide -- gossamer_hide + | OpMinimize -- gossamer_minimize + | OpMaximize -- gossamer_maximize + | OpRestore -- gossamer_restore (from Minimized or Maximized) + | OpRequestClose -- gossamer_request_close (signals intent; window stays open) + | OpRun -- gossamer_run (event loop; CONSUMES the handle) + | OpDestroy -- gossamer_destroy (immediate teardown; CONSUMES the handle) + +-------------------------------------------------------------------------------- +-- Valid Transitions +-------------------------------------------------------------------------------- + +||| A proof that transitioning from state `s` via operation `op` leads to +||| state `t`. Each constructor witnesses one valid transition. +||| +||| Invariants encoded: +||| - Closed is the only absorbing state (no constructor has source Closed). +||| - OpRun and OpDestroy always lead to Closed. +||| - OpRequestClose does NOT change the window state (it merely signals the +||| shell to ask the user for confirmation; the transition to Closed happens +||| only when the user confirms via OpRun/OpDestroy). +public export +data WindowTransition : (s : WindowState) -> (op : WindowOp) -> (t : WindowState) -> Type where + -- show: Created → Visible, Hidden → Visible + ShowFromCreated : WindowTransition Created OpShow Visible + ShowFromHidden : WindowTransition Hidden OpShow Visible + + -- hide: Visible → Hidden + HideFromVisible : WindowTransition Visible OpHide Hidden + + -- minimize: Visible → Minimized + MinimizeFromVisible : WindowTransition Visible OpMinimize Minimized + + -- maximize: Visible → Maximized + MaximizeFromVisible : WindowTransition Visible OpMaximize Maximized + + -- restore: Minimized → Visible, Maximized → Visible + RestoreFromMinimized : WindowTransition Minimized OpRestore Visible + RestoreFromMaximized : WindowTransition Maximized OpRestore Visible + + -- requestClose: visible states remain (user confirmation pending) + RequestCloseVisible : WindowTransition Visible OpRequestClose Visible + RequestCloseHidden : WindowTransition Hidden OpRequestClose Hidden + RequestCloseMinimized : WindowTransition Minimized OpRequestClose Minimized + RequestCloseMaximized : WindowTransition Maximized OpRequestClose Maximized + + -- run (blocking event loop): any non-Closed state → Closed + RunFromCreated : WindowTransition Created OpRun Closed + RunFromVisible : WindowTransition Visible OpRun Closed + RunFromHidden : WindowTransition Hidden OpRun Closed + RunFromMinimized : WindowTransition Minimized OpRun Closed + RunFromMaximized : WindowTransition Maximized OpRun Closed + + -- destroy (immediate teardown): any non-Closed state → Closed + DestroyFromCreated : WindowTransition Created OpDestroy Closed + DestroyFromVisible : WindowTransition Visible OpDestroy Closed + DestroyFromHidden : WindowTransition Hidden OpDestroy Closed + DestroyFromMinimized : WindowTransition Minimized OpDestroy Closed + DestroyFromMaximized : WindowTransition Maximized OpDestroy Closed + +-------------------------------------------------------------------------------- +-- GS1-INV-1: Closed is a terminal state +-------------------------------------------------------------------------------- + +||| No transition is valid from the Closed state. +||| +||| Proof: by exhaustive case analysis on `WindowTransition Closed op t`. +||| Every constructor of WindowTransition has a source state other than Closed, +||| so the type `WindowTransition Closed op t` is uninhabited for all op, t. +public export +closedIsTerminal : WindowTransition Closed op t -> Void +closedIsTerminal _ impossible + +-------------------------------------------------------------------------------- +-- GS1-INV-2: Borrow classification +-------------------------------------------------------------------------------- + +||| A borrow operation does not change the window state and does not destroy it. +||| These are the "safe" operations that read or write window properties. +||| +||| Borrow operations: loadHTML, navigate, eval, setTitle, resize, show, hide, +||| minimize, maximize, restore, requestClose. +||| Consuming operations: run, destroy. +public export +data IsBorrow : WindowOp -> Type where + BorrowShow : IsBorrow OpShow + BorrowHide : IsBorrow OpHide + BorrowMinimize : IsBorrow OpMinimize + BorrowMaximize : IsBorrow OpMaximize + BorrowRestore : IsBorrow OpRestore + BorrowRequestClose : IsBorrow OpRequestClose + +public export +data IsConsuming : WindowOp -> Type where + ConsumingRun : IsConsuming OpRun + ConsumingDestroy : IsConsuming OpDestroy + +||| Borrow and consuming are disjoint: no operation is both. +public export +borrowNotConsuming : IsBorrow op -> IsConsuming op -> Void +borrowNotConsuming BorrowShow x = case x of {} +borrowNotConsuming BorrowHide x = case x of {} +borrowNotConsuming BorrowMinimize x = case x of {} +borrowNotConsuming BorrowMaximize x = case x of {} +borrowNotConsuming BorrowRestore x = case x of {} +borrowNotConsuming BorrowRequestClose x = case x of {} + +||| A consuming operation always leads to Closed. +public export +consumingLeadsToClosed + : IsConsuming op + -> WindowTransition s op t + -> t = Closed +consumingLeadsToClosed ConsumingRun RunFromCreated = Refl +consumingLeadsToClosed ConsumingRun RunFromVisible = Refl +consumingLeadsToClosed ConsumingRun RunFromHidden = Refl +consumingLeadsToClosed ConsumingRun RunFromMinimized = Refl +consumingLeadsToClosed ConsumingRun RunFromMaximized = Refl +consumingLeadsToClosed ConsumingDestroy DestroyFromCreated = Refl +consumingLeadsToClosed ConsumingDestroy DestroyFromVisible = Refl +consumingLeadsToClosed ConsumingDestroy DestroyFromHidden = Refl +consumingLeadsToClosed ConsumingDestroy DestroyFromMinimized = Refl +consumingLeadsToClosed ConsumingDestroy DestroyFromMaximized = Refl + +-------------------------------------------------------------------------------- +-- GS1-INV-3: Reachability from Created +-------------------------------------------------------------------------------- + +||| Proof that a state is reachable from Created via a (possibly empty) sequence +||| of transitions. Encoded as a path in the state machine. +public export +data ReachableFrom : (origin : WindowState) -> (dest : WindowState) -> Type where + ||| Every state is reachable from itself (zero steps). + RFRefl : ReachableFrom s s + ||| If dest is reachable from origin, and there is a valid transition from + ||| dest via some op to next, then next is reachable from origin. + RFStep : ReachableFrom origin dest + -> WindowTransition dest op next + -> ReachableFrom origin next + +||| All six window states are reachable from Created. +public export +visibleReachable : ReachableFrom Created Visible +visibleReachable = RFStep RFRefl ShowFromCreated + +public export +hiddenReachable : ReachableFrom Created Hidden +hiddenReachable = RFStep visibleReachable HideFromVisible + +public export +minimizedReachable : ReachableFrom Created Minimized +minimizedReachable = RFStep visibleReachable MinimizeFromVisible + +public export +maximizedReachable : ReachableFrom Created Maximized +maximizedReachable = RFStep visibleReachable MaximizeFromVisible + +public export +closedReachable : ReachableFrom Created Closed +closedReachable = RFStep RFRefl RunFromCreated + +-------------------------------------------------------------------------------- +-- GS1-INV-4: Window state is Active iff not Closed +-------------------------------------------------------------------------------- + +||| Predicate: the window is "active" (not closed). +public export +data IsActive : WindowState -> Type where + ActiveCreated : IsActive Created + ActiveVisible : IsActive Visible + ActiveHidden : IsActive Hidden + ActiveMinimized : IsActive Minimized + ActiveMaximized : IsActive Maximized + +||| Closed windows are not active. +public export +closedNotActive : IsActive Closed -> Void +closedNotActive x = case x of {} + +||| Every non-Closed state is active. Takes a proof that `s` is not +||| `Closed` (the original `s = Closed -> Void -> IsActive s` signature +||| was ill-formed: `notClosed` had type `s = Closed`, so `notClosed Refl` +||| did not type-check; the intended contract is `Not (s = Closed)`). +public export +nonClosedIsActive : (s : WindowState) -> Not (s = Closed) -> IsActive s +nonClosedIsActive Created notClosed = ActiveCreated +nonClosedIsActive Visible notClosed = ActiveVisible +nonClosedIsActive Hidden notClosed = ActiveHidden +nonClosedIsActive Minimized notClosed = ActiveMinimized +nonClosedIsActive Maximized notClosed = ActiveMaximized +nonClosedIsActive Closed notClosed = absurd (notClosed Refl) + +||| A borrow transition preserves the Active property. +public export +borrowPreservesActive + : IsBorrow op + -> WindowTransition s op t + -> IsActive s + -> IsActive t +borrowPreservesActive BorrowShow ShowFromCreated _ = ActiveVisible +borrowPreservesActive BorrowShow ShowFromHidden _ = ActiveVisible +borrowPreservesActive BorrowHide HideFromVisible _ = ActiveHidden +borrowPreservesActive BorrowMinimize MinimizeFromVisible _ = ActiveMinimized +borrowPreservesActive BorrowMaximize MaximizeFromVisible _ = ActiveMaximized +borrowPreservesActive BorrowRestore RestoreFromMinimized _ = ActiveVisible +borrowPreservesActive BorrowRestore RestoreFromMaximized _ = ActiveVisible +borrowPreservesActive BorrowRequestClose RequestCloseVisible _ = ActiveVisible +borrowPreservesActive BorrowRequestClose RequestCloseHidden _ = ActiveHidden +borrowPreservesActive BorrowRequestClose RequestCloseMinimized _ = ActiveMinimized +borrowPreservesActive BorrowRequestClose RequestCloseMaximized _ = ActiveMaximized diff --git a/tests/README.adoc b/tests/README.adoc index ecfe682..8f8917d 100644 --- a/tests/README.adoc +++ b/tests/README.adoc @@ -1,4 +1,4 @@ -// SPDX-License-Identifier: MPL-2.0 +// SPDX-License-Identifier: CC-BY-SA-4.0 = Tests Gossamer's test suites, organised by language per the project rule