Skip to content

Commit 0ab4218

Browse files
Jonathan D.A. Jewellclaude
Jonathan D.A. Jewell
and
claude
committed
chore: sync template files and configuration
Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
1 parent 7e4b260 commit 0ab4218

11 files changed

Lines changed: 973 additions & 1 deletion

File tree

‎.github/PROVEN-INTEGRATION.md‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
1+
# proven Integration Plan
2+
3+
This document outlines the recommended [proven](https://github.com/hyperpolymath/proven) modules for ECHIDNA.
4+
5+
## Recommended Modules
6+
7+
| Module | Purpose | Priority |
8+
|--------|---------|----------|
9+
| SafeGraph | Directed graphs with cycle detection proofs for proof dependency tracking | High |
10+
| SafeOrdering | Temporal ordering with causality proofs for proof step sequencing | High |
11+
| SafeConsensus | Distributed consensus with quorum proofs for multi-prover agreement | High |
12+
13+
## Integration Notes
14+
15+
ECHIDNA as a neurosymbolic theorem proving platform supporting 12 provers requires formally verified proof management:
16+
17+
- **SafeGraph** models proof dependencies as DAGs. The `Acyclic` proof guarantees no circular dependencies in proof chains, and `topoSort` provides correct ordering for proof verification. `PathExists` verifies lemma reachability.
18+
19+
- **SafeOrdering** sequences proof steps with verified causality. When combining proofs from multiple provers, the vector clock implementation ensures steps are merged in the correct order. `CausalDelivery` guarantees proper ordering of distributed proof events.
20+
21+
- **SafeConsensus** enables multi-prover agreement. When multiple provers (Coq, Lean, Agda, etc.) verify the same theorem, `Quorum` proves sufficient agreement, and `Agreement` proves all agreeing provers have the same result.
22+
23+
As ECHIDNA already uses proven for its Idris 2 proofs (see `Proven/FFI/Echidna.idr`), these modules extend that integration to the proof orchestration layer.
24+
25+
## Related
26+
27+
- [proven library](https://github.com/hyperpolymath/proven)
28+
- [Idris 2 documentation](https://idris2.readthedocs.io/)
29+
- [ECHIDNA-proven FFI](https://github.com/hyperpolymath/proven/blob/main/src/Proven/FFI/Echidna.idr)

‎.github/workflows/rust.yml‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
name: Rust
3+
4+
on:
5+
push:
6+
branches: [ "main" ]
7+
pull_request:
8+
branches: [ "main" ]
9+
10+
env:
11+
CARGO_TERM_COLOR: always
12+
13+
jobs:
14+
build:
15+
16+
runs-on: ubuntu-latest
17+
18+
steps:
19+
- uses: actions/checkout@v4
20+
- name: Build
21+
run: cargo build --verbose
22+
- name: Run tests
23+
run: cargo test --verbose

‎CHANGELOG.md‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
<!--
2+
SPDX-License-Identifier: MIT AND Palimpsest-0.6
3+
SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
4+
-->
5+
6+
# Changelog
7+
8+
All notable changes to the ECHIDNA project will be documented in this file.
9+
10+
The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
11+
and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
12+
13+
## [Unreleased]
14+
15+
### Added
16+
- RSR/CCCP compliance templates
17+
- Dual licensing (MIT + Palimpsest v0.6)
18+
- REUSE-compliant SPDX headers
19+
- GitLab CI/CD pipeline with security scanning
20+
- Podman containerization support
21+
- Justfile build system
22+
- Complete project documentation structure
23+
24+
### Changed
25+
- Nothing yet
26+
27+
### Deprecated
28+
- Nothing yet
29+
30+
### Removed
31+
- Nothing yet
32+
33+
### Fixed
34+
- Nothing yet
35+
36+
### Security
37+
- Integrated Trivy security scanning
38+
- Added cargo-audit for Rust dependencies
39+
- Implemented Aqua.jl for Julia package security
40+
41+
## [0.1.0] - 2025-11-22
42+
43+
### Added
44+
- Initial project structure
45+
- Rust core implementation
46+
- Julia ML components
47+
- ReScript UI foundation
48+
- Basic Agda prover support
49+
- Project documentation (CLAUDE.md)
50+
- Contribution guidelines
51+
- Code of Conduct
52+
- Security policy
53+
54+
### Infrastructure
55+
- GitLab CI/CD pipeline
56+
- Podman Containerfile
57+
- REUSE license compliance
58+
- EditorConfig for consistent formatting
59+
- .gitignore for all languages
60+
61+
### Documentation
62+
- Comprehensive README
63+
- CONTRIBUTING guide
64+
- CODE_OF_CONDUCT
65+
- SECURITY policy
66+
- CHANGELOG (this file)
67+
- AUTHORS attribution
68+
69+
## Release Notes Format
70+
71+
Each release will include the following sections as applicable:
72+
73+
### Added
74+
- New features and capabilities
75+
76+
### Changed
77+
- Changes to existing functionality
78+
79+
### Deprecated
80+
- Features that will be removed in future releases
81+
82+
### Removed
83+
- Features that have been removed
84+
85+
### Fixed
86+
- Bug fixes
87+
88+
### Security
89+
- Security improvements and vulnerability fixes
90+
91+
## Version Numbering
92+
93+
ECHIDNA follows Semantic Versioning (SemVer):
94+
95+
- **MAJOR** version (X.0.0): Incompatible API changes
96+
- **MINOR** version (0.X.0): New functionality, backwards compatible
97+
- **PATCH** version (0.0.X): Bug fixes, backwards compatible
98+
99+
## Upcoming Releases
100+
101+
### [0.2.0] - Target: 2026-01-22
102+
- Tier 1 prover implementations (Coq, Lean, Isabelle)
103+
- Enhanced Z3 and CVC5 integration
104+
- Neural proof synthesis improvements
105+
- Python to Julia migration completion
106+
107+
### [0.3.0] - Target: 2026-04-22
108+
- Tier 2 prover implementations (Metamath, HOL Light, Mizar)
109+
- Aspect tagging system
110+
- OpenCyc integration
111+
112+
### [0.4.0] - Target: 2026-07-22
113+
- Tier 3 prover implementations (PVS, ACL2)
114+
- DeepProbLog integration
115+
- Performance optimizations
116+
117+
### [1.0.0] - Target: 2026-11-22
118+
- Tier 4 prover implementation (HOL4)
119+
- Complete 12-prover support
120+
- Production-ready release
121+
- Comprehensive documentation
122+
123+
## Migration Notes
124+
125+
### From Quill (Agda-only)
126+
127+
If you're migrating from the original Quill project:
128+
129+
1. Update import paths to use ECHIDNA modules
130+
2. Replace Python ML code with Julia equivalents
131+
3. Update prover selection to use new universal backend
132+
4. Review aspect tagging configuration
133+
5. Update build scripts to use Justfile
134+
135+
See migration guide in docs/ for detailed instructions.
136+
137+
---
138+
139+
**Maintained By**: ECHIDNA Project Team
140+
**Last Updated**: 2025-11-22

‎CONTRIBUTING.md‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Contributing
2+
3+
See [CONTRIBUTING.adoc](CONTRIBUTING.adoc) for full contribution guidelines.

‎LICENSE.txt‎

Lines changed: 153 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,153 @@
1+
SPDX-License-Identifier: PMPL-1.0
2+
SPDX-FileCopyrightText: 2024-2025 Palimpsest Stewardship Council
3+
4+
================================================================================
5+
PALIMPSEST-MPL LICENSE VERSION 1.0
6+
================================================================================
7+
8+
File-level copyleft with ethical use and quantum-safe provenance
9+
10+
Based on Palimpsest-MPL License v1.0 (PMPL-1.0)
11+
12+
--------------------------------------------------------------------------------
13+
PREAMBLE
14+
--------------------------------------------------------------------------------
15+
16+
This License extends the Palimpsest-MPL License v1.0 (PMPL-1.0) (PMPL-1.0) with provisions
17+
for ethical use, post-quantum cryptographic provenance, and emotional lineage
18+
protection. The base PMPL-1.0 terms apply except where explicitly modified by
19+
the Exhibits below.
20+
21+
Like a palimpsest manuscript where each layer builds upon what came before,
22+
this license recognizes that creative works carry history, context, and meaning
23+
that transcend mere code or text.
24+
25+
--------------------------------------------------------------------------------
26+
SECTION 1: BASE LICENSE
27+
--------------------------------------------------------------------------------
28+
29+
This License incorporates the full text of Palimpsest-MPL License v1.0 (PMPL-1.0) by
30+
reference. The complete PMPL-1.0 text is available at:
31+
https://github.com/hyperpolymath/palimpsest-license
32+
33+
All terms, conditions, and definitions from PMPL-1.0 apply except where
34+
explicitly modified by the Exhibits in this License.
35+
36+
--------------------------------------------------------------------------------
37+
SECTION 2: ADDITIONAL DEFINITIONS
38+
--------------------------------------------------------------------------------
39+
40+
2.1. "Emotional Lineage"
41+
means the narrative, cultural, symbolic, and contextual meaning embedded
42+
in Covered Software, including but not limited to: protest traditions,
43+
cultural heritage, trauma narratives, and community stories.
44+
45+
2.2. "Provenance Metadata"
46+
means cryptographically signed attribution information attached to or
47+
associated with Covered Software, including author identities, timestamps,
48+
modification history, and lineage references.
49+
50+
2.3. "Non-Interpretive System"
51+
means any automated system that processes Covered Software without
52+
preserving or considering its Emotional Lineage, including but not
53+
limited to: AI training pipelines, content aggregators, and automated
54+
summarization tools.
55+
56+
2.4. "Quantum-Safe Signature"
57+
means a cryptographic signature using algorithms resistant to attacks
58+
by quantum computers, as specified in Exhibit B.
59+
60+
--------------------------------------------------------------------------------
61+
SECTION 3: ETHICAL USE REQUIREMENTS
62+
--------------------------------------------------------------------------------
63+
64+
In addition to the rights and obligations under PMPL-1.0:
65+
66+
3.1. Emotional Lineage Preservation
67+
You must make reasonable efforts to preserve and communicate the
68+
Emotional Lineage of Covered Software when distributing or creating
69+
derivative works. This includes maintaining narrative context, cultural
70+
attributions, and symbolic meaning where documented.
71+
72+
3.2. Non-Interpretive System Notice
73+
If You use Covered Software as input to a Non-Interpretive System, You
74+
must:
75+
(a) document such use in a publicly accessible manner; and
76+
(b) not claim that outputs of such systems carry the Emotional Lineage
77+
of the original work without explicit permission from Contributors.
78+
79+
3.3. Ethical Use Declaration
80+
Commercial use of Covered Software requires acknowledgment that You have
81+
read and understood Exhibit A (Ethical Use Guidelines) and agree to act
82+
in good faith accordance with its principles.
83+
84+
See Exhibit A for complete Ethical Use Guidelines.
85+
86+
--------------------------------------------------------------------------------
87+
SECTION 4: PROVENANCE REQUIREMENTS
88+
--------------------------------------------------------------------------------
89+
90+
4.1. Metadata Preservation
91+
You must not strip, alter, or obscure Provenance Metadata from Covered
92+
Software except where technically necessary and with clear documentation
93+
of any changes.
94+
95+
4.2. Quantum-Safe Provenance (Optional)
96+
Contributors may sign their Contributions using Quantum-Safe Signatures.
97+
If Quantum-Safe Signatures are present, You must preserve them in all
98+
distributions.
99+
100+
4.3. Lineage Chain
101+
When creating derivative works, You should extend the provenance chain
102+
to include Your own contributions, maintaining cryptographic linkage to
103+
prior Contributors where feasible.
104+
105+
See Exhibit B for Quantum-Safe Provenance specifications.
106+
107+
--------------------------------------------------------------------------------
108+
SECTION 5: GOVERNANCE
109+
--------------------------------------------------------------------------------
110+
111+
5.1. Stewardship Council
112+
This License is maintained by the Palimpsest Stewardship Council, which
113+
may issue clarifications, interpretive guidance, and future versions.
114+
115+
5.2. Version Selection
116+
You may use Covered Software under this version of the License or any
117+
later version published by the Palimpsest Stewardship Council.
118+
119+
5.3. Dispute Resolution
120+
Disputes regarding interpretation of Ethical Use Requirements (Section 3)
121+
should first be submitted to the Palimpsest Stewardship Council for
122+
non-binding guidance before pursuing legal remedies.
123+
124+
--------------------------------------------------------------------------------
125+
SECTION 6: COMPATIBILITY
126+
--------------------------------------------------------------------------------
127+
128+
6.1. PMPL-1.0 Compatibility
129+
Covered Software under this License may be combined with software under
130+
PMPL-1.0. The combined work must comply with both licenses.
131+
132+
6.2. Secondary Licenses
133+
The Secondary License provisions of PMPL-1.0 Section 3.3 apply to this
134+
License.
135+
136+
--------------------------------------------------------------------------------
137+
EXHIBITS
138+
--------------------------------------------------------------------------------
139+
140+
Exhibit A - Ethical Use Guidelines
141+
Exhibit B - Quantum-Safe Provenance Specification
142+
143+
See separate files:
144+
- EXHIBIT-A-ETHICAL-USE.txt
145+
- EXHIBIT-B-QUANTUM-SAFE.txt
146+
147+
--------------------------------------------------------------------------------
148+
END OF PALIMPSEST-MPL LICENSE VERSION 1.0
149+
--------------------------------------------------------------------------------
150+
151+
For questions about this License:
152+
- Repository: https://github.com/hyperpolymath/palimpsest-license
153+
- Council: contact via repository Issues

‎LICENSES/MIT.txt‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,21 @@
1+
MIT License
2+
3+
Copyright (c) 2024-2025 ECHIDNA Project Contributors
4+
5+
Permission is hereby granted, free of charge, to any person obtaining a copy
6+
of this software and associated documentation files (the "Software"), to deal
7+
in the Software without restriction, including without limitation the rights
8+
to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
9+
copies of the Software, and to permit persons to whom the Software is
10+
furnished to do so, subject to the following conditions:
11+
12+
The above copyright notice and this permission notice shall be included in all
13+
copies or substantial portions of the Software.
14+
15+
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
16+
IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
17+
FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
18+
AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
19+
LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
20+
OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
21+
SOFTWARE.

0 commit comments

Comments
 (0)