Repository navigation
chore(license): migrate to AGPL-3.0-or-later - #112
Merged
Merged
Conversation
Replace LICENSE file with canonical AGPL-3.0-or-later text and update package metadata (Cargo.toml/package.json/deno.json/mix.exs/pyproject.toml where present) to declare the new SPDX identifier. Rationale: Joshua co-dev. Part of estate-wide metadata cleanup 2026-05-26.
hyperpolymath
enabled auto-merge (squash)
May 26, 2026 13:23
🔍 Hypatia Security ScanFindings: 166 issues detected
View findings[
{
"reason": "Workflow executes remote script directly (curl/wget piped to shell). Download, verify checksum/signature, then execute.",
"type": "download_then_run",
"file": "mirror.yml",
"action": "verify_download_integrity",
"rule_module": "workflow_audit",
"severity": "high"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echidna/echidna/proofs/agda/Basic.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (2 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echidna/echidna/proofs/agda/SoundnessPreservation.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "Agda postulate assumes without proof -- potential soundness hole (1 occurrences, CWE-704)",
"type": "agda_postulate",
"file": "/home/runner/work/echidna/echidna/meta-checker/src/Echidna/AxiomSafety.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "UNSOUND: --type-in-type collapses type hierarchy (Girard's paradox) (1 occurrences, CWE-704)",
"type": "agda_type_in_type",
"file": "/home/runner/work/echidna/echidna/meta-checker/src/Echidna/AxiomSafety.agda",
"action": "flag",
"rule_module": "code_safety",
"severity": "critical"
},
{
"reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
"type": "lean_axiom",
"file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/IntegrityVerification.lean",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
"type": "lean_axiom",
"file": "/home/runner/work/echidna/echidna/verification/proofs/lean4/ConfidenceLattice.lean",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
"type": "lean_axiom",
"file": "/home/runner/work/echidna/echidna/proofs/lean/mvp_basic.lean",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "User-defined axiom -- not verified by Lean kernel (1 occurrences, CWE-704)",
"type": "lean_axiom",
"file": "/home/runner/work/echidna/echidna/proofs/lean/Propositional.lean",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
},
{
"reason": "Nickel file missing SPDX-License-Identifier header (1 occurrences, CWE-1104)",
"type": "ncl_missing_spdx",
"file": "/home/runner/work/echidna/echidna/configs/config.ncl",
"action": "flag",
"rule_module": "code_safety",
"severity": "medium"
}
]Powered by Hypatia Neurosymbolic CI/CD Intelligence |
This was referenced May 30, 2026
hyperpolymath
added a commit
that referenced
this pull request
May 30, 2026
The estate's check-trusted-base.sh (standards#203) flagged 12 markers on main since #112 (2026-05-28) — all 12 are detector-pattern false positives, structurally identical to the believe_me FP audit recorded in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)" (21 hits, zero real escapes). Resolution: * 10 Rust hits across 4 files are pattern-detector tables. Each holds a `Vec<DangerousPattern>` (or equivalent) that *enumerates* the very `unsafePerformIO` / `unsafeCoerce` / `Obj.magic` strings the scanner is hunting. The scanner's naive substring grep can't tell "uses the pattern" from "names the pattern in a detector table". Added a new `.trusted-base-ignore` (whole-path exemption, format mirrors the scanner's documented spec) covering the four files: - src/rust/verification/axiom_tracker.rs - crates/echidna-core-spark/src/axiom_tracker.rs - src/rust/corpus/agda.rs - src/rust/corpus/idris2.rs * 2 Agda postulates are real well-justified axioms: - `funext` (function extensionality) in proofs/agda/Basic.agda - `Conflicts` (abstract parameter) in proofs/agda/SoundnessPreservation.agda Both already had INTENTIONAL AXIOM / INTENTIONAL PARAMETER prose documentation, but outside the script's 5-line preceding-marker window. Added an `-- AXIOM:` / `-- TRUSTED:` magic-word line immediately before each `postulate` so the scanner sees it. Effect: `governance / Trusted-base reduction policy` should now report [OK] (12 markers exempted via .trusted-base-ignore + inline magic), up from the 12/12 undocumented failure on main. Refs: #92 (broader baseline failures, this PR addresses the trusted-base slice only).
3 tasks done
8 tasks done
hyperpolymath
added a commit
that referenced
this pull request
Oct 14, 2026
…w linter (#437) ## Summary The copied "Verify immutable action lockfile" step in `workflow-linter.yml` pins its own gh-actions-lock **v0.1.6**, which cannot read lockfile **v0.0.3**. Every current `gh actions-lock` writes v0.0.3, so the step fails the first time a current tool refreshes this repo's lock. That has already happened in proof-burrower (#111/#112 there). The step was also a second verifier with a second version pin. Governance already verifies the lock through standards `scripts/update-actions-lock.sh`. This repo's governance pin (571cc734) runs it inside its workflow-lint job. That is one tested implementation, with one pin, and it accepts reusable-workflow coverage. Owner decision 2026-10-14 (selector): drop the lock step from copied linters, and move the estate to gh-actions-lock v0.2.0 (metadatastician/standards#1250). Pilot repos first: proof-burrower, echidna, echidnabot. ## Changes - `.github/workflows/workflow-linter.yml`: the pinned-binary lock step is replaced by a comment pointing at the governance gate. The issue-regression and allow-fail steps are unchanged. - No `uses:` changes, so `actions.lock` is untouched. ## RSR Quality Checklist ### Required - [x] Tests pass: `scripts/ci/test-issue-regressions.sh` passes. - [x] Code is formatted (n/a, YAML only). - [x] Linter is clean: actionlint v1.7.7 clean; the workflow duplicate-key check is clean. - [x] No banned language patterns. - [x] No `unsafe` blocks without `// SAFETY:` comments (n/a). - [x] No banned functions (n/a). - [x] SPDX license headers present on all new/modified source files. - [x] No secrets, credentials, or `.env` files included. ## Testing - Standards `update-actions-lock.sh --verify-local` on this branch passes (exit 0) under both gh-actions-lock v0.1.6 and v0.2.0. - `lint-workflows` is green on `main` today. This removes the failure before it happens rather than fixing a red check. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- _Generated by [Claude Code](https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3)_ Co-authored-by: Claude <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Migrates this repo's license declaration from
MPL-2.0toAGPL-3.0-or-later.Rationale: Joshua co-dev.
Changes
AGPL-3.0-or-latertext (including SPDX header).Part of estate-wide metadata cleanup 2026-05-26.