diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 6f2de427..251dad16 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -108,7 +108,7 @@ package definitions (not metadata files) and must NOT be deleted. | **Guile Scheme** | Guix package definitions (`guix.scm`, `manifests/*.scm`) | `.scm` metadata files are deprecated — see below | | **Bash/POSIX Shell** | Build scripts, CI glue | Keep minimal | | **AffineScript** | TEA sources in `src/ui/tea/`; static shell in `src/ui/public/` | The compile pipeline is unavailable; `build-ui` fails explicitly | -| **Bun** | Estate JavaScript runtime | The legacy serve recipes still require migration; open `src/ui/public/prove.html` directly for the working static UI | +| **Bun** | Estate JavaScript runtime | `just serve-ui` serves the static shell via `scripts/serve-static.js` (Bun) | | **JavaScript** | Build tooling only (Tailwind config, test harness) | Not for business logic | | **OCaml** | AffineScript compiler host | Decision locked — AffineScript selected for UI | | **Nickel** | Configuration language | Used across `configs/`, `echidna-playground/contractiles/k9/`, `.machine_readable/`, `echidnabot/config/` (11+ `.ncl` files) | diff --git a/.echidnabot.toml b/.echidnabot.toml index 7406ca4a..9df6ff54 100644 --- a/.echidnabot.toml +++ b/.echidnabot.toml @@ -27,7 +27,7 @@ coq = { enabled = true, priority = "low" } lean = { enabled = true, priority = "low" } [provers.idris2] -package_file = "src/abi/echidna.ipkg" +package_file = "src/abi/echidnaabi.ipkg" source_dirs = ["src/abi"] totality_required = true coverage_required = true diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index fb9afafe..5f4f3571 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,7 +6,7 @@ # Core prover backends /src/rust/provers/ @hyperpolymath -/src/rust/core.rs @hyperpolymath +/src/rust/lib.rs @hyperpolymath /src/rust/dispatch.rs @hyperpolymath # ML layer diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml new file mode 100644 index 00000000..79dd5dad --- /dev/null +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -0,0 +1,91 @@ +# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +{ + name: "Bug report", + description: "Something behaves differently from what it claims to do.", + labels: [ + "bug", + "needs-triage", + ], + body: [ + { + type: "markdown", + attributes: { + value: "Please report what you **observed**, not what you inferred. A command and\nits actual output is worth more than a description of the problem.\n", + }, + }, + { + type: "textarea", + id: "what-happened", + attributes: { + label: "What happened", + description: "The observed behaviour, with the exact command and its output.", + placeholder: "$ just verify\nerror: ...\n", + render: "shell", + }, + validations: { + required: true, + }, + }, + { + type: "textarea", + id: "expected", + attributes: { + label: "What you expected instead", + }, + validations: { + required: true, + }, + }, + { + type: "textarea", + id: "repro", + attributes: { + label: "Minimal reproduction", + description: "The shortest sequence that reproduces it from a clean checkout.", + }, + validations: { + required: true, + }, + }, + { + type: "input", + id: "version", + attributes: { + label: "Version / commit", + description: "Output of `git rev-parse --short HEAD`.", + }, + validations: { + required: true, + }, + }, + { + type: "textarea", + id: "environment", + attributes: { + label: "Environment", + description: "OS, and the output of `just --version` and `mise current` if relevant.", + }, + validations: { + required: false, + }, + }, + { + type: "checkboxes", + id: "checks", + attributes: { + label: "Before submitting", + options: [ + { + label: "I have reported observed output rather than a summary of it.", + required: true, + }, + { + label: "This is not a security vulnerability (those go via a private advisory).", + required: true, + }, + ], + }, + }, + ], +} diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 00000000..ede0a5dd --- /dev/null +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -0,0 +1,20 @@ +# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Issue chooser configuration. Blank issues stay enabled so that reports which +# fit neither form are not silently discouraged. +{ + blank_issues_enabled: true, + contact_links: [ + { + name: "Security vulnerability", + url: "https://github.com/hyperpolymath/echidna/security/advisories/new", + about: "Report privately via a security advisory. Do NOT open a public issue.", + }, + { + name: "Question or support request", + url: "https://github.com/hyperpolymath/echidna/discussions", + about: "Ask a question. See .github/SUPPORT.md for what to expect.", + }, + ], +} diff --git a/.github/ISSUE_TEMPLATE/feature_request.yml b/.github/ISSUE_TEMPLATE/feature_request.yml new file mode 100644 index 00000000..4f998640 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/feature_request.yml @@ -0,0 +1,60 @@ +# SPDX-License-Identifier: CC-BY-SA-4.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +{ + name: "Feature request", + description: "Propose a capability this project does not yet have.", + labels: [ + "enhancement", + "needs-triage", + ], + body: [ + { + type: "textarea", + id: "problem", + attributes: { + label: "The problem", + description: "What are you unable to do today? Describe the situation, not the solution.", + }, + validations: { + required: true, + }, + }, + { + type: "textarea", + id: "proposal", + attributes: { + label: "Proposed change", + }, + validations: { + required: true, + }, + }, + { + type: "textarea", + id: "alternatives", + attributes: { + label: "Alternatives considered", + description: "Including doing nothing — say why that is insufficient.", + }, + validations: { + required: false, + }, + }, + { + type: "dropdown", + id: "scope", + attributes: { + label: "Scope", + description: "Would this change the template's shape, and therefore every repo minted from it?", + options: [ + "Repo-local — affects only this project", + "Template-wide — would propagate to minted repos", + "Not sure", + ], + }, + validations: { + required: true, + }, + }, + ], +} diff --git a/SECURITY.md b/.github/SECURITY.md similarity index 83% rename from SECURITY.md rename to .github/SECURITY.md index 4bc2c5fa..6946d419 100644 --- a/SECURITY.md +++ b/.github/SECURITY.md @@ -5,4 +5,4 @@ Report vulnerabilities privately using [GitHub Security Advisories](https://gith If GitHub is unavailable, contact the maintainer at j.d.a.jewell@open.ac.uk. Do not disclose vulnerabilities in public issues. -The full policy, supported versions, requested report details, and response timelines are maintained in [SECURITY.adoc](SECURITY.adoc). +The full policy, supported versions, requested report details, and response timelines are maintained in [SECURITY.adoc](../SECURITY.adoc). diff --git a/.github/SUPPORT.md b/.github/SUPPORT.md new file mode 100644 index 00000000..8f47f4cd --- /dev/null +++ b/.github/SUPPORT.md @@ -0,0 +1,7 @@ +# Support + +For questions, help, and community discussion: + +- GitHub Discussions: https://github.com/hyperpolymath/echidna/discussions +- GitHub Issues: https://github.com/hyperpolymath/echidna/issues +- Documentation: See README.adoc in the root directory. diff --git a/.github/canonical-references/prover-counts.yml b/.github/canonical-references/prover-counts.yml index 45c1646e..f0de876c 100644 --- a/.github/canonical-references/prover-counts.yml +++ b/.github/canonical-references/prover-counts.yml @@ -13,38 +13,35 @@ # # Rule format documented in the upstream step comment. -id: prover-counts -description: | - Bare prover counts (variants vs impl files vs advertised vs core) - in narrative-carrying top-level docs must defer to - docs/PROVER_COUNT.adoc so they cannot drift. Patterns are anchored - with (^|[[:space:]]) so neighbours like Tier-1, v1.2.3, port 8081 - don't false-positive. - -patterns: - - '(^|[[:space:]])[0-9]+[[:space:]]+prover[[:space:]]+backends?\b' - - '(^|[[:space:]])[0-9]+[[:space:]]*-[[:space:]]*prover[[:space:]]+core\b' - - '(^|[[:space:]])[0-9]+[[:space:]]+core[[:space:]]+(backends?|provers?)\b' - - '(^|[[:space:]])[0-9]+[[:space:]]+(backends?|provers?)[[:space:]]+(operational|advertised|implemented|available|across|total)\b' - - '(^|[[:space:]])[0-9]+[[:space:]]+ProverKind[[:space:]]+variants?\b' - - '(^|[[:space:]])[0-9]+[[:space:]]+backend[[:space:]]+implementation[[:space:]]+files?\b' - - '(^|[[:space:]])[0-9]+/[0-9]+[[:space:]]+(backends?|provers?)\b' - -canonical_pointer: docs/PROVER_COUNT.adoc - -scope: - include: - - README.md - - README.adoc - - EXPLAINME.adoc - - CLAUDE.md - - CONTRIBUTING.md - - ../../.github/CONTRIBUTING.md - - QUICKSTART-USER.adoc - - QUICKSTART-DEV.adoc - - QUICKSTART-MAINTAINER.adoc - - RSR_COMPLIANCE.adoc - - SECURITY.md - - MAINTAINERS.adoc - - AUTHORS.adoc - - CODE_OF_CONDUCT.adoc +{ + id: "prover-counts", + description: "Bare prover counts (variants vs impl files vs advertised vs core)\nin narrative-carrying top-level docs must defer to\ndocs/PROVER_COUNT.adoc so they cannot drift. Patterns are anchored\nwith (^|[[:space:]]) so neighbours like Tier-1, v1.2.3, port 8081\ndon't false-positive.\n", + patterns: [ + "(^|[[:space:]])[0-9]+[[:space:]]+prover[[:space:]]+backends?\\b", + "(^|[[:space:]])[0-9]+[[:space:]]*-[[:space:]]*prover[[:space:]]+core\\b", + "(^|[[:space:]])[0-9]+[[:space:]]+core[[:space:]]+(backends?|provers?)\\b", + "(^|[[:space:]])[0-9]+[[:space:]]+(backends?|provers?)[[:space:]]+(operational|advertised|implemented|available|across|total)\\b", + "(^|[[:space:]])[0-9]+[[:space:]]+ProverKind[[:space:]]+variants?\\b", + "(^|[[:space:]])[0-9]+[[:space:]]+backend[[:space:]]+implementation[[:space:]]+files?\\b", + "(^|[[:space:]])[0-9]+/[0-9]+[[:space:]]+(backends?|provers?)\\b", + ], + canonical_pointer: "docs/PROVER_COUNT.adoc", + scope: { + include: [ + "README.md", + "README.adoc", + "EXPLAINME.adoc", + "CLAUDE.md", + "CONTRIBUTING.md", + "../../.github/CONTRIBUTING.md", + "QUICKSTART-USER.adoc", + "QUICKSTART-DEV.adoc", + "QUICKSTART-MAINTAINER.adoc", + "RSR_COMPLIANCE.adoc", + "SECURITY.adoc", + "MAINTAINERS.adoc", + "AUTHORS.adoc", + "CODE_OF_CONDUCT.adoc", + ], + }, +} diff --git a/.github/copilot-instructions.md b/.github/copilot-instructions.md new file mode 100644 index 00000000..4d214967 --- /dev/null +++ b/.github/copilot-instructions.md @@ -0,0 +1,89 @@ + + + + +# Copilot Instructions + +## Before Writing Code + +- Read `.machine_readable/descriptiles/` (STATE, META, ECOSYSTEM) for canonical + file locations. echidna has not yet migrated these into a `*_chora.deed`. +- State files (.a2ml) live in `.machine_readable/` ONLY, never the root. + +## License + +- SPDX: `MPL-2.0` on all new files. +- Never use AGPL-3.0. +- Copyright: `Jonathan D.A. Jewell (hyperpolymath) ` + +## Code Style + +- Use descriptive variable names. +- Annotate and document all files. +- Add SPDX header to every source file. +- Use `just` for build/test/lint commands. + +## Banned Patterns + +- Idris2: no `believe_me`, no `assert_total` +- Haskell: no `unsafeCoerce`, no `unsafePerformIO` +- OCaml: no `Obj.magic` +- Coq: no `Admitted` +- Lean: no `sorry` +- Rust: no `transmute` unless FFI with `// SAFETY:` comment + +## JavaScript / TypeScript runtimes + +Ordered preference (`standards/3-practice/LANGUAGE-POLICY.adoc` §1) — reach for the first +that can do the job: + +1. **Bun** — default for all new work. Runs compiled ESM/JS directly, no bundler + step. Uses an npm-compatible `package.json` plus `bun.lock`; both are + expected, not anti-patterns. +2. **pnpm** — only where an upstream toolchain requires `node_modules`. +3. **npm** — last resort. Permitted, never preferred; a deliberate, noted choice. + +**Deno is being removed**, not grandfathered. Owner ruling 2026-08-26: *"deno is +to go and bun is the way we are going, put it first everywhere unless not +possible and explain why if not."* Existing Deno projects migrate to Bun; where +Bun genuinely cannot be used, document the reason in the repo. + +**TypeScript is not the language for new application code — AffineScript is.** +`LANGUAGE-POLICY.adoc` §1.2, ruled 2026-08-25, separates two questions the older +text ran together: *runtime* is Bun (where `.ts` runs at all, Bun runs it), while +the *language* target is AffineScript. TypeScript is permitted only where +AffineScript cannot reach — the same narrow, transitional carve-out JavaScript +holds for MCP protocol glue and runtime APIs. ReScript remains banned; its +migration destination is AffineScript. + +## Banned Languages + +- No Go (use Rust) +- No Python (use Julia or Rust) +- No Nix (use Guix) +- No Deno for new work — being removed estate-wide; use Bun (owner ruling 2026-08-26) +- No ReScript (`LANGUAGE-POLICY.adoc` §3) — migrate to AffineScript + +## Containers + +- Use Podman, never Docker. +- Name the file `Containerfile`, never `Dockerfile`. +- Base image: `cgr.dev/chainguard/wolfi-base:latest`. + +## ABI/FFI + +- ABI definitions in Idris2 (`src/abi/`, package `src/abi/echidnaabi.ipkg`). +- FFI implementations in Zig (`ffi/zig/`, `src/zig_ffi/`). +- echidna keeps its own ABI/FFI layout rather than the template's interface tree. + +## State Files + +The retired STATE/META/ECOSYSTEM/AGENTIC/CLADE `.a2ml` files must not be +recreated anywhere; their content is in the repo deed (`*_chora.deed`) and +`docs/status/ROADMAP.adoc`. + +Never create NEUROSYM.a2ml or PLAYBOOK.a2ml in the repo root. +They belong in `.machine_readable/` only. diff --git a/.github/copilot/coding-agent.yml b/.github/copilot/coding-agent.yml index a719a773..8568867d 100644 --- a/.github/copilot/coding-agent.yml +++ b/.github/copilot/coding-agent.yml @@ -1,6 +1,16 @@ -mcp_servers: - boj-server: - command: npx - args: ["-y", "@hyperpolymath/boj-server@latest"] - env: - BOJ_URL: http://localhost:7700 +# SPDX-License-Identifier: MPL-2.0 +# Copilot coding-agent MCP servers, launched with bunx (Bun is the estate +# JavaScript runtime). +{ + mcp_servers: { + boj-server: { + command: "bunx", + args: [ + "@hyperpolymath/boj-server@latest", + ], + env: { + BOJ_URL: "http://localhost:7700", + }, + }, + }, +} diff --git a/.github/dependabot.yml b/.github/dependabot.yml index 94bf53d8..cbe5b884 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -1,22 +1,49 @@ # SPDX-License-Identifier: MPL-2.0 -version: 2 -updates: - - package-ecosystem: "cargo" - directory: "/" - schedule: - interval: "weekly" - ignore: - - dependency-name: "*" - update-types: ["version-update:semver-patch"] - - package-ecosystem: "github-actions" - directory: "/" - schedule: - interval: "weekly" - groups: - actions: - patterns: - - "*" - - package-ecosystem: "npm" - directory: "/" - schedule: - interval: "weekly" +# Dependabot configuration for echidna (KYAML; format with +# standards/scripts/kyaml-format.sh). Only ecosystems present in the repo are +# listed: there is no package.json, so the former `npm` block only produced +# failing "npm_and_yarn" update runs. +# +# github-actions: Dependabot rewrites `uses:` refs but cannot touch +# .github/workflows/actions.lock. A bump PR therefore needs `gh actions-lock` +# run on its branch before it can merge; the governance "Actions lockfile +# verify" and lint-workflows checks go red until it is. The codeql-action +# hold mirrors rsr-template-repo: the trailing `*` is load-bearing because +# workflows use the init/analyze subpaths, which Dependabot names separately. +# +# cargo: `open-pull-requests-limit: 0` stops routine version PRs but keeps +# security PRs flowing (an `ignore: semver-patch` rule would also silence +# patch-level security fixes). +{ + version: 2, + updates: [ + { + package-ecosystem: "github-actions", + directory: "/", + schedule: { + interval: "weekly", + }, + groups: { + actions: { + patterns: [ + "*", + ], + }, + }, + open-pull-requests-limit: 2, + ignore: [ + { + dependency-name: "github/codeql-action*", + }, + ], + }, + { + package-ecosystem: "cargo", + directory: "/", + schedule: { + interval: "weekly", + }, + open-pull-requests-limit: 0, + }, + ], +} diff --git a/.github/funding.yml b/.github/funding.yml deleted file mode 100644 index e4f7c077..00000000 --- a/.github/funding.yml +++ /dev/null @@ -1,4 +0,0 @@ -# Funding Configuration -# See: https://docs.github.com/en/repositories/managing-your-repositorys-custom-fields/displaying-a-sponsor-button-in-your-repository - -github: metadatastician diff --git a/.github/pull_request_template.md b/.github/pull_request_template.md new file mode 100644 index 00000000..9af74b3c --- /dev/null +++ b/.github/pull_request_template.md @@ -0,0 +1,48 @@ + +## Summary + + + +## Changes + + + +- + +## RSR Quality Checklist + + + +### Required + +- [ ] Tests pass (`just test` or equivalent) +- [ ] Code is formatted (`just fmt` or equivalent) +- [ ] Linter is clean (no new warnings or errors) +- [ ] No banned language patterns (no , no npm/bun, no Go/Python) +- [ ] No `unsafe` blocks without `// SAFETY:` comments +- [ ] No banned functions (`believe_me`, `unsafeCoerce`, `Obj.magic`, `Admitted`, `sorry`) +- [ ] SPDX license headers present on all new/modified source files +- [ ] No secrets, credentials, or `.env` files included + +### As Applicable + +- [ ] Repo deed (`*_chora.deed`) `(status)` / `(maturity)` updated (if project state changed) +- [ ] Repo deed `(ecosystem)` updated (if integrations changed) +- [ ] Repo deed `(meta)` and/or `docs/decisions/` updated (if architectural decisions changed) +- [ ] `docs/status/ROADMAP.adoc` updated (if milestones or next actions changed) +- [ ] Documentation updated for user-facing changes +- [ ] `TOPOLOGY.md` updated (if architecture changed) +- [ ] `CHANGELOG` or release notes updated +- [ ] New dependencies reviewed for license compatibility (MPL-2.0 / MPL-2.0) +- [ ] ABI/FFI changes validated (`src/abi/` and `ffi/zig/` consistent) + +## Testing + + + +## Screenshots + + diff --git a/.github/rulesets/Immutable-Tags.json b/.github/rulesets/Immutable-Tags.json new file mode 100644 index 00000000..75fe73a0 --- /dev/null +++ b/.github/rulesets/Immutable-Tags.json @@ -0,0 +1,28 @@ +{ + "name": "Immutable-Tags", + "target": "tag", + "enforcement": "active", + "conditions": { + "ref_name": { + "include": [ + "~ALL" + ], + "exclude": [] + } + }, + "bypass_actors": [], + "rules": [ + { + "type": "deletion" + }, + { + "type": "non_fast_forward" + }, + { + "type": "update" + }, + { + "type": "required_signatures" + } + ] +} diff --git a/.github/rulesets/README.adoc b/.github/rulesets/README.adoc new file mode 100644 index 00000000..572f9347 --- /dev/null +++ b/.github/rulesets/README.adoc @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// Copyright (c) 2026 Jonathan D.A. Jewell += Repository rulesets + +[IMPORTANT] +==== +**GitHub does not read this directory.** Unlike `.github/workflows/`, +`.github/dependabot.yml` or `.github/settings.yml`, ruleset JSON in a repository +path is *not* auto-applied by any GitHub feature. These files are +**documentation of intent plus a ready-to-POST payload** — nothing more. + +A ruleset only takes effect once someone applies it via the REST API or imports +it in the web UI. Until then the protection described here **is not in force**. +==== + +== Applying a ruleset + +Per ADR-0003 the *Configure* stage is an operator stage: identity, visibility and +branch/tag protection are set out of band. Automation is future work and must not +be described as existing. + +[source,bash] +---- +# Apply (create) a ruleset on the current repo: +gh api --method POST \ + -H "Accept: application/vnd.github+json" \ + "/repos/{owner}/{repo}/rulesets" \ + --input .github/rulesets/base.json + +# List what is actually in force — the only authoritative answer: +gh api "/repos/{owner}/{repo}/rulesets" --jq '.[] | "\(.id)\t\(.name)\t\(.enforcement)"' + +# Update an existing ruleset in place (needs its numeric id from the list above): +gh api --method PUT \ + "/repos/{owner}/{repo}/rulesets/" \ + --input .github/rulesets/base.json +---- + +== Files + +`base.json`:: Canonical branch protection ruleset for the default branch (`~DEFAULT_BRANCH`). +Enforces deleted-branch protection, linear history, squash merge, signatures and required +status checks, without unsatisfiable coverage or deadlocking approval requirements. +Sourced verbatim from `hyperpolymath/standards` `config/rulesets/base.json` (§7.3). + +`branch-floor.json`:: The irreducible branch floor for the default branch: deletion and +non-fast-forward protection only, with no bypass actors. This is the ruleset that keeps a +branch recoverable when the richer `Base` ruleset is unavailable or has been removed. +Sourced verbatim from `hyperpolymath/standards` `config/rulesets/branch-floor.json`. + +`require-signed-commits.json`:: Standalone, zero-bypass `required_signatures` on the default +branch (D215). Every new repo is born with it. See `hyperpolymath/standards` +`docs/SIGNING-POLICY.adoc`. Sourced verbatim from `config/rulesets/require-signed-commits.json`. + +`require-linear-history.json`:: Standalone, zero-bypass `required_linear_history` (D216). +Pair it with squash-only merge settings. A new repo starts with no merge commits, so it is +always linear-safe. Sourced verbatim from `config/rulesets/require-linear-history.json`. + +`Immutable-Tags.json`:: Makes release tags immutable — blocks tag deletion, +non-fast-forward updates, and overwrites, and requires signed tags. + +[NOTE] +==== +Files here are named to match the *live ruleset name*, which is not always the +upstream filename. Upstream ships `branch-floor.json` and `immutable-tags.json` +(lowercase, with a matching lowercase `name` inside the JSON); this repository's +`Immutable-Tags.json` declares `"name": "Immutable-Tags"`. Renaming a file here +changes nothing on GitHub, but it does change which upstream file it is diffed +against — keep that in mind when syncing. +==== + +== What is actually enforced on this repository + +Files are intent; this table is fact. Regenerate it with: + +[source,bash] +---- +gh api "/repos/{owner}/{repo}/rulesets" --jq '.[] | "\(.id)\t\(.name)\t\(.enforcement)\t\(.target)"' +---- + +|=== +| Live ruleset | Enforcement | Target | Covers + +| `Base` | active | branch | deletion, required signatures, code scanning (CodeQL/Hypatia), Copilot review, non-fast-forward +| `Branch-Floor` | active | branch | deletion, non-fast-forward +| `Immutable-Tags` | active | tag | creation, deletion, non-fast-forward, update, required signatures +|=== + +=== Known drift between these files and what is live + +The files below are *not* a transcript of the live rulesets. This is the +divergence as of 2026-09-28, recorded rather than silently reconciled because +`base.json` is sourced verbatim from upstream and must not be forked here. + +*Live `Base` rule that no file describes* :: + +`code_scanning` (with CodeQL and Hypatia tools) and `copilot_code_review` are +enforced live but appear in neither `base.json` nor any upstream file synced into +this directory. Upstream's nearest equivalent, +`config/rulesets/Optimus-Extras.json`, declares `code_scanning` with an *empty* +`code_scanning_tools` list, so it does not describe what is live here either. + +*Removed from live `Base` on 2026-10-02 (owner decision)* :: + +`Scorecard` was dropped from `code_scanning_tools`, and the `code_coverage` rule +(minimum 80%, max drop 5) was deleted. Neither could ever be satisfied by a pull +request. `scorecard.yml` runs only on `schedule` and `workflow_dispatch`, and +Scorecard scores repository posture rather than a diff, so with +`alerts_threshold: all` any standing finding would have blocked every PR. Nothing +in this template produces a coverage report: `rust-ci / llvm-cov` is skipped +because the template has no Rust. The result was that every PR sat `BLOCKED` until +an admin bypass (#219). CodeQL and Hypatia both upload results on pull requests, +so they stay. Do not add either rule back without a producer that runs on +`pull_request`. + +*`base.json` rules that are not in force* :: + +`required_linear_history` is in `base.json` but not in live `Base`; it is +enforced by the separate `Require-Linear-History` ruleset. `required_status_checks` (an empty list, so a no-op) and the +`pull_request` rule are likewise absent from live `Base`. (`non_fast_forward` is +live in `Base` as of 2026-10-02, and is also covered by `Branch-Floor`.) + +*`Immutable-Tags.json` lags the live ruleset* :: + +The live tag ruleset includes a `creation` rule; this file does not. Upstream +`immutable-tags.json` also populates `bypass_actors` (repository-role 5 and an +integration) with `bypass_mode: always`, and this file declares none. + +[WARNING] +==== +`bypass_actors` cannot be diffed from a low-privilege token: the REST API returns +`null` for that field unless the caller has admin on the repository. Absence of +`bypass_actors` in the output above is *not* evidence that none are configured. +==== + +== Verifying + +Do not infer that a ruleset is active because the JSON is present. Check with the +`gh api ... /rulesets` list above. A ruleset that exists as a file but was never +POSTed is the protection equivalent of a check that cannot fail. + +Conversely, do not infer that the estate is protected because a ruleset exists. +A ruleset with `enforcement: disabled` is inert, and a `pull_request` rule with +`allowed_merge_methods: []` can never be satisfied at all. diff --git a/.github/rulesets/base.json b/.github/rulesets/base.json new file mode 100644 index 00000000..136c0a0d --- /dev/null +++ b/.github/rulesets/base.json @@ -0,0 +1,102 @@ +{ + "name": "Base", + "target": "branch", + "enforcement": "active", + "conditions": { + "ref_name": { + "include": [ + "~DEFAULT_BRANCH" + ], + "exclude": [] + } + }, + "bypass_actors": [ + { + "actor_id": 5, + "actor_type": "RepositoryRole", + "bypass_mode": "pull_request" + }, + { + "actor_id": 1236702, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 29110, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 15368, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 347564, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 46505, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 1143301, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 1144995, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 12526, + "actor_type": "Integration", + "bypass_mode": "pull_request" + }, + { + "actor_id": 2538504, + "actor_type": "Integration", + "bypass_mode": "pull_request" + } + ], + "rules": [ + { + "type": "deletion" + }, + { + "type": "non_fast_forward" + }, + { + "type": "required_signatures" + }, + { + "type": "required_linear_history" + }, + { + "type": "pull_request", + "parameters": { + "required_approving_review_count": 0, + "dismiss_stale_reviews_on_push": true, + "require_code_owner_review": false, + "require_last_push_approval": false, + "required_review_thread_resolution": true, + "require_extra_approval_for_unattributed_changes": false, + "required_reviewers": [], + "allowed_merge_methods": [ + "squash" + ] + } + }, + { + "type": "required_status_checks", + "parameters": { + "strict_required_status_checks_policy": true, + "do_not_enforce_on_create": false, + "required_status_checks": [] + } + } + ] +} diff --git a/.github/rulesets/branch-floor.json b/.github/rulesets/branch-floor.json new file mode 100644 index 00000000..465908ac --- /dev/null +++ b/.github/rulesets/branch-floor.json @@ -0,0 +1,16 @@ +{ + "name": "Branch-Floor", + "target": "branch", + "enforcement": "active", + "bypass_actors": [], + "conditions": { + "ref_name": { + "include": ["~DEFAULT_BRANCH"], + "exclude": [] + } + }, + "rules": [ + { "type": "deletion" }, + { "type": "non_fast_forward" } + ] +} diff --git a/.github/rulesets/require-linear-history.json b/.github/rulesets/require-linear-history.json new file mode 100644 index 00000000..188cca91 --- /dev/null +++ b/.github/rulesets/require-linear-history.json @@ -0,0 +1,19 @@ +{ + "name": "Require-Linear-History", + "target": "branch", + "enforcement": "active", + "bypass_actors": [], + "conditions": { + "ref_name": { + "include": [ + "~DEFAULT_BRANCH" + ], + "exclude": [] + } + }, + "rules": [ + { + "type": "required_linear_history" + } + ] +} diff --git a/.github/rulesets/require-signed-commits.json b/.github/rulesets/require-signed-commits.json new file mode 100644 index 00000000..01d8875c --- /dev/null +++ b/.github/rulesets/require-signed-commits.json @@ -0,0 +1,19 @@ +{ + "name": "Require-Signed-Commits", + "target": "branch", + "enforcement": "active", + "bypass_actors": [], + "conditions": { + "ref_name": { + "include": [ + "~DEFAULT_BRANCH" + ], + "exclude": [] + } + }, + "rules": [ + { + "type": "required_signatures" + } + ] +} diff --git a/.github/settings.yml b/.github/settings.yml index d7d037d5..7eed228b 100644 --- a/.github/settings.yml +++ b/.github/settings.yml @@ -45,110 +45,125 @@ # ─── Repository Settings ─────────────────────────────────────────────────────── -repository: - has_issues: true - has_projects: true - has_wiki: false - has_downloads: true - default_branch: main - allow_squash_merge: true - allow_merge_commit: true - allow_rebase_merge: true - delete_branch_on_merge: true - enable_automated_security_fixes: true - enable_vulnerability_alerts: true - -# ─── Labels ──────────────────────────────────────────────────────────────────── - -labels: - - name: "bug" - color: "d73a4a" - description: "Something isn't working" - - - name: "enhancement" - color: "a2eeef" - description: "New feature or request" - - - name: "documentation" - color: "0075ca" - description: "Improvements or additions to documentation" - - - name: "security" - color: "e4e669" - description: "Security-related issue or vulnerability" - - - name: "good first issue" - color: "7057ff" - description: "Good for newcomers" - - - name: "help wanted" - color: "008672" - description: "Extra attention is needed" - - - name: "question" - color: "d876e3" - description: "Further information is requested" - - - name: "duplicate" - color: "cfd3d7" - description: "This issue or pull request already exists" - - - name: "invalid" - color: "e4e669" - description: "This doesn't seem right" - - - name: "wontfix" - color: "ffffff" - description: "This will not be worked on" - - - name: "dependencies" - color: "0366d6" - description: "Pull requests that update a dependency file" - - - name: "ci/cd" - color: "fbca04" - description: "Continuous integration and deployment" - - - name: "rsr" - color: "006b75" - description: "Rhodium Standard Repository compliance" - - - name: "hypatia" - color: "5319e7" - description: "Hypatia neurosymbolic scanner finding" - - - name: "bot" - color: "b4a8d1" - description: "Automated action by gitbot-fleet" - - - name: "breaking-change" - color: "b60205" - description: "Introduces a breaking change" - - - name: "performance" - color: "f9d0c4" - description: "Performance improvement" - - - name: "refactor" - color: "c5def5" - description: "Code refactoring with no functional change" - +{ + repository: { + has_issues: true, + has_projects: true, + has_wiki: true, + has_downloads: true, + default_branch: "main", + allow_squash_merge: true, + allow_merge_commit: true, + allow_rebase_merge: false, + delete_branch_on_merge: true, + enable_automated_security_fixes: true, + enable_vulnerability_alerts: true, + }, + # ─── Labels ──────────────────────────────────────────────────────────────────── + labels: [ + { + name: "bug", + color: "d73a4a", + description: "Something isn't working", + }, + { + name: "enhancement", + color: "a2eeef", + description: "New feature or request", + }, + { + name: "documentation", + color: "0075ca", + description: "Improvements or additions to documentation", + }, + { + name: "security", + color: "e4e669", + description: "Security-related issue or vulnerability", + }, + { + name: "good first issue", + color: "7057ff", + description: "Good for newcomers", + }, + { + name: "help wanted", + color: "008672", + description: "Extra attention is needed", + }, + { + name: "question", + color: "d876e3", + description: "Further information is requested", + }, + { + name: "duplicate", + color: "cfd3d7", + description: "This issue or pull request already exists", + }, + { + name: "invalid", + color: "e4e669", + description: "This doesn't seem right", + }, + { + name: "wontfix", + color: "ffffff", + description: "This will not be worked on", + }, + { + name: "dependencies", + color: "0366d6", + description: "Pull requests that update a dependency file", + }, + { + name: "ci/cd", + color: "fbca04", + description: "Continuous integration and deployment", + }, + { + name: "rsr", + color: "006b75", + description: "Rhodium Standard Repository compliance", + }, + { + name: "hypatia", + color: "5319e7", + description: "Hypatia neurosymbolic scanner finding", + }, + { + name: "bot", + color: "b4a8d1", + description: "Automated action by gitbot-fleet", + }, + { + name: "breaking-change", + color: "b60205", + description: "Introduces a breaking change", + }, + { + name: "performance", + color: "f9d0c4", + description: "Performance improvement", + }, + { + name: "refactor", + color: "c5def5", + description: "Code refactoring with no functional change", + }, + ], +} # ─── Branch Protection ───────────────────────────────────────────────────────── - -branches: - - name: "main" - protection: - required_pull_request_reviews: - required_approving_review_count: 1 - dismiss_stale_reviews: true - require_code_owner_reviews: true - required_status_checks: - strict: true - contexts: - - "hypatia-scan" - - "codeql" - enforce_admins: true - required_signatures: true - restrictions: null - allow_force_pushes: false - allow_deletions: false +# +# Deliberately absent. Branch rules for `main` live in repository rulesets +# (payloads in .github/rulesets/, applied with `gh api`), which is what +# `squabble verify-satisfied` and AGENTS.md §5a read. A classic-protection +# block here duplicated them, required a code-owner approval that a +# single-maintainer repo cannot give, and named contexts ("hypatia-scan", +# "codeql") that no workflow reports under those names. +# +# Merge policy: squash by default, never rebase (rebase-merge replays commits unsigned and breaks +# required_signatures). Merge commits stay enabled only for proof PRs whose +# commit series must survive (owner ruling 2026-09-30, AGENTS.md §5c item 6); +# squash is the default form. Wiki on: the forge wiki is +# published from docs/wikis/. diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index a8bd4490..8110298e 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -6,7 +6,7 @@ workflows: '.github/workflows/agda-meta-checker.yml': - 'actions/cache@v6.1.0' - 'actions/checkout@v7.0.1' - - 'haskell-actions/setup@v2.12.0' + - 'haskell-actions/setup@v2.12.1' '.github/workflows/boj-build.yml': - 'actions/checkout@v7.0.1' '.github/workflows/bridge-gate.yml': @@ -27,7 +27,7 @@ workflows: - 'swatinem/rust-cache@v2.9.2' '.github/workflows/codeql.yml': - 'actions/checkout@v7.0.1' - - 'github/codeql-action@v4.38.1' + - 'github/codeql-action@v4.38.2' '.github/workflows/container-ci.yml': - 'actions/checkout@v7.0.1' '.github/workflows/dogfood-gate.yml': @@ -58,7 +58,7 @@ workflows: - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' - 'swatinem/rust-cache@v2.9.2' - - 'taiki-e/install-action@v2.87.13' + - 'taiki-e/install-action@v2.87.22' '.github/workflows/pages.yml': - 'actions/checkout@v7.0.1' - 'actions/deploy-pages@v5.0.1' @@ -66,17 +66,15 @@ workflows: '.github/workflows/proof-safety.yml': - 'actions/checkout@v7.0.1' - 'swatinem/rust-cache@v2.9.2' - '.github/workflows/rust-ci.yml': [] - '.github/workflows/rust-native-reusable.yml': + '.github/workflows/rust-ci.yml': - 'actions/checkout@v7.0.1' - - 'dtolnay/rust-toolchain@v1' - - 'goto-bus-stop/setup-zig@v2.2.1' + - 'dtolnay/rust-toolchain@master' - 'swatinem/rust-cache@v2.9.2' '.github/workflows/s4-loop.yml': - 'actions/checkout@v7.0.1' - 'dtolnay/rust-toolchain@v1' - 'swatinem/rust-cache@v2.9.2' - - 'taiki-e/install-action@v2.87.13' + - 'taiki-e/install-action@v2.87.22' '.github/workflows/scorecard.yml': [] '.github/workflows/secret-scanner.yml': [] '.github/workflows/security-scan.yml': [] @@ -85,6 +83,11 @@ workflows: - 'dtolnay/rust-toolchain@v1' - 'swatinem/rust-cache@v2.9.2' '.github/workflows/spark-theatre-gate.yml': [] + '.github/workflows/static-analysis-gate.yml': + - 'actions/checkout@v7.0.1' + - 'actions/download-artifact@v8.0.1' + - 'actions/upload-artifact@v7.0.1' + - 'erlef/setup-beam@v1.24.1' '.github/workflows/verification-proofs-cron.yml': - 'actions/checkout@v7.0.1' '.github/workflows/workflow-linter.yml': @@ -139,14 +142,24 @@ dependencies: repo_id: 496012378 uses: - 'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f' + 'dtolnay/rust-toolchain@master': + ref: 'master' + commit: 'sha1-02cb101ec7c40f2c49e1d9714d64511d8e1b74de' + owner_id: 1940490 + repo_id: 260749683 'dtolnay/rust-toolchain@v1': ref: 'v1' commit: 'sha1-02cb101ec7c40f2c49e1d9714d64511d8e1b74de' owner_id: 1940490 repo_id: 260749683 - 'github/codeql-action@v4.38.1': - ref: 'v4.38.1' - commit: 'sha1-1c5b675653bb5c22dbe9b12b556ec555138e09fd' + 'erlef/setup-beam@v1.24.1': + ref: 'v1.24.1' + commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' + owner_id: 47606891 + repo_id: 331103973 + 'github/codeql-action@v4.38.2': + ref: 'v4.38.2' + commit: 'sha1-2892aa5e19bbd11bc0cff5427e3b750a04d9e3c2' owner_id: 9919 repo_id: 259445878 'google/clusterfuzzlite@v1': @@ -154,14 +167,9 @@ dependencies: commit: 'sha1-884713a6c30a92e5e8544c39945cd7cb630abcd1' owner_id: 1342004 repo_id: 400046858 - 'goto-bus-stop/setup-zig@v2.2.1': - ref: 'v2.2.1' - commit: 'sha1-abea47f85e598557f500fa1fd2ab7464fcb39406' - owner_id: 1006268 - repo_id: 212984112 - 'haskell-actions/setup@v2.12.0': - ref: 'v2.12.0' - commit: 'sha1-6037f33647c3f17758a2356c80fc4a53d7e0685d' + 'haskell-actions/setup@v2.12.1': + ref: 'v2.12.1' + commit: 'sha1-0f8e8c99d88aeb3fbfd523f1ef2c6f762d10d64d' owner_id: 75048950 repo_id: 623796603 'mlugg/setup-zig@v2.2.1': @@ -174,63 +182,8 @@ dependencies: commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' owner_id: 580492 repo_id: 298565987 - 'taiki-e/install-action@v2.87.13': - ref: 'v2.87.13' - commit: 'sha1-26e9283f268b880168bdbd2c545dfcd60ec2c6ab' + 'taiki-e/install-action@v2.87.22': + ref: 'v2.87.22' + commit: 'sha1-83ac0ad63c0167e6f06796fab0fce28db1bf3db0' owner_id: 43724913 repo_id: 442947557 - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9': - ref: 'v6.1.0' - commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9' - owner_id: 44036562 - repo_id: 215566462 - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1': - ref: 'v7.0.1' - commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' - owner_id: 44036562 - repo_id: 197814629 - 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a': - ref: 'v7.0.1' - commit: 'sha1-043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' - owner_id: 44036562 - repo_id: 192625955 - 'actions/upload-artifact@65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08': - ref: 'v4.6.0' - commit: 'sha1-65c4c4a1ddee5b72f698fdd19549f0f0fb45cf08' - owner_id: 44036562 - repo_id: 192625955 - 'denoland/setup-deno@22d081ff2d3a40755e97629de92e3bcbfa7cf2ed': - ref: 'v2.0.5' - commit: 'sha1-22d081ff2d3a40755e97629de92e3bcbfa7cf2ed' - owner_id: 42048915 - repo_id: 356423100 - 'dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772': - ref: 'stable' - commit: 'sha1-6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772' - owner_id: 1940490 - repo_id: 260749683 - 'editorconfig-checker/action-editorconfig-checker@840e866d93b8e032123c23bac69dece044d4d84c': - ref: 'v2.2.0' - commit: 'sha1-840e866d93b8e032123c23bac69dece044d4d84c' - owner_id: 26415196 - repo_id: 297874902 - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124': - ref: 'v1.24.1' - commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' - owner_id: 47606891 - repo_id: 331103973 - 'ossf/scorecard-action@2d1146689b8cda280b9bc96326124645441f03bc': - ref: 'v2.4.4' - commit: 'sha1-2d1146689b8cda280b9bc96326124645441f03bc' - owner_id: 67707773 - repo_id: 421101922 - 'softprops/action-gh-release@c95fe1489396fe8a9eb87c0abf8aa5b2ef267fda': - ref: 'v2.2.1' - commit: 'sha1-c95fe1489396fe8a9eb87c0abf8aa5b2ef267fda' - owner_id: 2242 - repo_id: 204253808 - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555': - ref: 'v0.10.0' - commit: 'sha1-e83874834305fe9a4a2997156cb26c5de65a8555' - owner_id: 135788 - repo_id: 208510314 diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index dfa3c927..49b64d63 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -5,31 +5,37 @@ # # formal-verification.yml — Creusot formal verification of the trust-pipeline kernel. # -# Stage 8c of the ECHIDNA ROADMAP. Both jobs are merge gates as of Stage 8c-M3. +# Stage 8c of the ECHIDNA ROADMAP. # -# stable-tests — `cargo test -p echidna-core-spark` on stable Rust. -# Exercises every proof obligation as a `#[test]` function. -# Fast (~10 s); always passes on a correct Rust installation. +# stable-tests — `cargo test -p echidna-core-creusot` on stable Rust. +# Exercises every stated proof obligation as a `#[test]`. +# Runs on every PR that touches the crate. # -# creusot-verify — `cargo +nightly creusot` with Why3 + Z3 discharge. -# Hard gate as of Stage 8c-M3. Requires Why3 in the runner; -# `apt-get install why3` covers Ubuntu 22.04+. -# If Why3 availability changes, re-evaluate whether to keep -# this as a required check or move to a scheduled/manual job. +# creusot-verify — `cargo creusot` with Why3 discharge. MANUAL ONLY +# (workflow_dispatch). It has never discharged an +# obligation: the crate does not yet depend on +# `creusot-contracts`, the nightly-2024-05-01 pin predates +# current Creusot, and `cargo install creusot` is not how +# Creusot is installed (it ships an INSTALL script that +# provisions why3/why3find via opam). Running it on every +# push only produced a red check that proved nothing. +# Re-enable on PRs once a dispatch run is green. Until then +# the annotations are STATED, NOT PROVED. # -# See crates/echidna-core-spark/CREUSOT-SETUP.adoc for local setup. +# See crates/echidna-core-creusot/CREUSOT-SETUP.adoc for local setup. name: Formal Verification (Stage 8c) on: pull_request: paths: - - 'crates/echidna-core-spark/**' + - 'crates/echidna-core-creusot/**' - '.github/workflows/formal-verification.yml' push: branches: [main] paths: - - 'crates/echidna-core-spark/**' + - 'crates/echidna-core-creusot/**' + workflow_dispatch: # Cause-B mitigation (#77): cancel superseded runs so stacked pushes # to the same ref don't pile up identical jobs in the queue. @@ -62,21 +68,17 @@ jobs: workspaces: ". -> target" - name: Run trust-pipeline invariant tests - run: cargo test -p echidna-core-spark --verbose + run: cargo test -p echidna-core-creusot --verbose env: RUST_BACKTRACE: 1 - # ── Job 2: Creusot formal verification (hard gate — Stage 8c-M3) ───────── + # ── Job 2: Creusot formal verification (manual; not yet a gate) ─────────── creusot-verify: - name: Creusot formal verification + name: Creusot formal verification (manual) + # Only on explicit dispatch — see the header for why this is not a gate. + if: ${{ github.event_name == 'workflow_dispatch' }} runs-on: ubuntu-latest timeout-minutes: 15 - # No continue-on-error — this is a hard merge gate as of Stage 8c-M3. - # The outer-loop invariant for compute is now live; all obligations - # (PO-1..P8, PO-A1..A12) must discharge under Why3+Z3. - # - # If this job becomes flaky due to nightly drift, update the pin in - # rust-toolchain.toml and the `toolchain:` field below together. steps: - name: Checkout repository @@ -85,7 +87,7 @@ jobs: - name: Install nightly Rust toolchain (Creusot pin) uses: dtolnay/rust-toolchain@v1 with: - # Pin matches crates/echidna-core-spark/rust-toolchain.toml. + # Pin matches crates/echidna-core-creusot/rust-toolchain.toml. # Update both files together when bumping. toolchain: nightly-2024-05-01 components: rustc, cargo, rust-src @@ -120,7 +122,7 @@ jobs: - name: Run Creusot verification run: | cargo +nightly-2024-05-01 creusot \ - -p echidna-core-spark \ + -p echidna-core-creusot \ -- \ --features creusot \ --why3 "$(which why3)" diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml index 7d6b4839..b3abae4e 100644 --- a/.github/workflows/rust-ci.yml +++ b/.github/workflows/rust-ci.yml @@ -1,12 +1,19 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 -# This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. -# This workflow is managed by gh actions-lock. -# Rust CI — thin wrapper calling the shared estate reusable in -# hyperpolymath/standards. Configure once, propagate everywhere. -# See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards. +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Rust CI for echidna: check + clippy + fmt, test, cargo audit, llvm-cov. +# +# Inlined from the former local reusable `rust-native-reusable.yml` +# (2026-10-05). Calling that reusable ended every run in a "workflow file +# issue" failure with zero jobs, both with tag refs and with SHA refs, while +# plain workflows in this repo (CodeQL, MVP smoke) start normally; actionlint +# and `gh actions-lock --no-fix` were clean. A plain workflow sidesteps it. +# The standards `rust-ci-reusable.yml` is not used because it does not +# install capnproto/protoc, which echidna-wire and echidna-grpc need. +# +# Job names carry the `rust-ci / ` prefix so the check contexts keep the +# estate's canonical Rust names. name: Rust CI on: @@ -14,13 +21,233 @@ on: branches: [main, master] pull_request: +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + permissions: - actions: read contents: read jobs: - rust-ci: - uses: ./.github/workflows/rust-native-reusable.yml # main 2026-08-04 (lockfile-bearing ref: actions.lock required by caller-side enforcement, standards#570) - with: - enable_audit: true - enable_coverage: true + # Skip the whole reusable when the repo has no Cargo.toml — lets consumers + # add the wrapper unconditionally without worrying about repos that don't + # ship Rust code yet. This MUST be a checked-out step, NOT a job-level + # `if: hashFiles(...)`: job `if:` is evaluated server-side before any + # checkout, so hashFiles() sees an empty workspace and always returns '' + # — which silently skipped every job on EVERY repo, Rust or not. The + # detect job checks out and exposes a real boolean the others gate on. + detect: + timeout-minutes: 5 + name: rust-ci / Detect Cargo.toml + runs-on: ubuntu-latest + permissions: + contents: read + outputs: + has_cargo: ${{ steps.detect.outputs.has_cargo }} + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + repository: ${{ github.repository }} + ref: ${{ github.ref }} + - name: Detect Cargo.toml + id: detect + run: | + if [ -f "./Cargo.toml" ]; then + echo "has_cargo=true" >> "$GITHUB_OUTPUT" + else + echo "has_cargo=false" >> "$GITHUB_OUTPUT" + fi + + check: + timeout-minutes: 20 + name: rust-ci / Cargo check + clippy + fmt + runs-on: ubuntu-latest + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + defaults: + run: + working-directory: . + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + repository: ${{ github.repository }} + ref: ${{ github.ref }} + + - name: Install Rust toolchain + # `toolchain:` is mandatory because the action is pinned by commit SHA: + # dtolnay/rust-toolchain infers the toolchain from the `@`-ref (e.g. + # `@stable`), but a SHA ref carries no version, so the action's "parse + # toolchain version" step fails with `'toolchain' is a required input`. + # See standards estate-wide rust-ci red. + uses: dtolnay/rust-toolchain@master + with: + toolchain: stable + components: clippy, rustfmt + + - name: Install native schema compilers + run: | + sudo apt-get update + sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev + + + - name: Cache cargo registry and build + uses: Swatinem/rust-cache@v2.9.2 + with: + workspaces: . + + - name: Cargo check + # `--locked` so CI honours `Cargo.lock` and surfaces dep drift the + # first push it happens, instead of silently re-resolving (which + # masked the echidna#92 / echidna PR #128 dependabot major-bump + # break for 24h). See standards#295. + run: cargo check --locked --all-targets + + - name: Cargo fmt + run: cargo fmt --all -- --check + + - name: Cargo clippy + run: cargo clippy --locked --all-targets -- -D warnings + + test: + timeout-minutes: 20 + name: rust-ci / Cargo test + runs-on: ubuntu-latest + needs: [detect, check] + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + defaults: + run: + working-directory: . + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + repository: ${{ github.repository }} + ref: ${{ github.ref }} + + - name: Install Rust toolchain + # `toolchain:` mandatory under SHA pin — see Cargo check job above. + uses: dtolnay/rust-toolchain@master + with: + toolchain: stable + + - name: Install native schema compilers + run: | + sudo apt-get update + sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev + + + - name: Cache cargo registry and build + uses: Swatinem/rust-cache@v2.9.2 + with: + workspaces: . + + - name: Run tests + # `--locked` — see Cargo check above. + run: cargo test --locked --all-targets + + - name: Write summary + if: always() + run: | + { + echo "## Rust CI Results" + echo "" + echo "- **cargo check**: ${{ needs.check.result }}" + echo "- **cargo test**: completed" + } >> "$GITHUB_STEP_SUMMARY" + + audit: + timeout-minutes: 20 + name: rust-ci / Cargo audit (security) + runs-on: ubuntu-latest + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + defaults: + run: + working-directory: . + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + repository: ${{ github.repository }} + ref: ${{ github.ref }} + + - name: Install Rust toolchain + # `toolchain:` mandatory under SHA pin — see Cargo check job above. + uses: dtolnay/rust-toolchain@master + with: + toolchain: stable + + - name: Install cargo-audit + # Use the binstall path when available to skip a from-source rebuild + # on every run — was the single biggest contributor to slow CI on + # repos that opted in to audit (~3–4 minute install). + run: cargo install cargo-audit --locked + + - name: Security audit + run: cargo audit + + coverage: + timeout-minutes: 25 + name: rust-ci / llvm-cov line coverage + runs-on: ubuntu-latest + needs: detect + if: ${{ needs.detect.outputs.has_cargo == 'true' }} + permissions: + contents: read + defaults: + run: + working-directory: . + env: + # Ratcheted line-coverage floor (from the caller). Raise toward target; never lower. + FLOOR: "0" + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + repository: ${{ github.repository }} + ref: ${{ github.ref }} + + - name: Install Rust toolchain + # `toolchain:` mandatory under SHA pin — see Cargo check job above. + uses: dtolnay/rust-toolchain@master + with: + toolchain: stable + components: llvm-tools-preview + + - name: Install native schema compilers + run: | + sudo apt-get update + sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev + + + - name: Install cargo-llvm-cov + run: cargo install cargo-llvm-cov --locked + + - name: Measure line coverage + id: cov + # Self-contained: no external coverage service. Own the gate on our runner. + run: | + set -euo pipefail + cargo llvm-cov --locked --json --output-path cov.json + PCT=$(jq -r '.data[0].totals.lines.percent' cov.json) + printf '### Line coverage: %.2f%% (floor %s%%)\n' "$PCT" "$FLOOR" >> "$GITHUB_STEP_SUMMARY" + echo "pct=$PCT" >> "$GITHUB_OUTPUT" + + - name: Enforce ratchet floor + run: | + set -euo pipefail + awk -v p="${{ steps.cov.outputs.pct }}" -v f="$FLOOR" 'BEGIN { + if (f !~ /^[0-9]+([.][0-9]+)?$/ || f + 0 > 100 || p !~ /^[0-9]+([.][0-9]+)?$/ || p + 0 > 100) { + print "FAIL: coverage and floor must be numeric percentages in [0, 100]"; exit 1 + } + if (p + 0 < f + 0) { printf "FAIL: line coverage %.2f%% is below floor %s%%\n", p, f; exit 1 } + printf "OK: line coverage %.2f%% >= floor %s%%\n", p, f + }' diff --git a/.github/workflows/rust-native-reusable.yml b/.github/workflows/rust-native-reusable.yml deleted file mode 100644 index e2213182..00000000 --- a/.github/workflows/rust-native-reusable.yml +++ /dev/null @@ -1,363 +0,0 @@ -# This workflow is managed by gh actions-lock. -# SPDX-License-Identifier: MPL-2.0 -# This workflow is managed by gh actions-lock. -# Derived from hyperpolymath/standards@571cc734cd69fb846032ec77a662aa8ee4fc32cd. -# Native workspace variant installs schema compilers before check/test/coverage. -# rust-ci-reusable.yml — Reusable Rust CI bundle (RSR). -# -# Replaces the per-repo `rust-ci.yml` template that copy-drifted across -# the estate. Estate audit (2026-05-26) found: -# -# * 137 repos shipping their own copy of rust-ci.yml -# * 30 unique SHAs — same logical workflow, drifted independently -# * Recurring failure modes across PRs: missing top-level -# `permissions:`, inconsistent `if: hashFiles('Cargo.toml')` -# guards, `cargo audit` re-installing every run, license-header -# drift (PMPL/MPL/AGPL), inconsistent SHA pins. -# -# The reusable bundles the union of features observed across the -# variants and gates the slow extras (audit, coverage) behind opt-in -# inputs so consumers only pay for what they want. -# -# Caller example (single wrapper, mirrors governance.yml + deno-ci.yml): -# -# jobs: -# rust-ci: -# uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef -# -# With audit + coverage enabled: -# -# jobs: -# rust-ci: -# uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef -# with: -# enable_audit: true -# enable_coverage: true -# zig_version: "0.15.2" # for Rust crates with a Zig-native build -# -# Sub-crate / monorepo workspace (Cargo.toml lives in a subdirectory): -# -# jobs: -# rust-ci-cli: -# uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef -# with: -# working_directory: crates/cli -# rust-ci-server: -# uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@70cdad0e95bb2366a9b2ae9789c0e377fef6e3ef -# with: -# working_directory: crates/server -# -# Out-of-scope (left bespoke per-repo): multi-OS matrices, cross-compile -# (`cross build`), multi-Rust-version matrices. Each has too much per-repo -# variance to share a single abstraction cleanly (verified against the 5 -# matrix-using repos as of 2026-05-26: julia-the-viper / verisimdb / -# verisimiser / reasonably-good-token-vault use four different matrix -# dimensions). - -name: Rust CI (native workspace) - -on: - workflow_call: - inputs: - runs-on: - description: Runner label for all Rust CI jobs - type: string - required: false - default: ubuntu-latest - enable_audit: - description: Run `cargo audit` (slow — installs each run; off by default) - type: boolean - required: false - default: false - enable_coverage: - description: Measure line coverage with cargo-llvm-cov and enforce `coverage_floor` (off by default) - type: boolean - required: false - default: false - coverage_floor: - description: Minimum line-coverage percent when enable_coverage is set; ratchet upward, never lower. - type: string - required: false - default: "0" - clippy_args: - description: Args appended to `cargo clippy` - type: string - required: false - default: "--all-targets -- -D warnings" - test_args: - description: Args appended to `cargo test` - type: string - required: false - default: "--all-targets" - check_args: - description: Args appended to `cargo check` - type: string - required: false - default: "--all-targets" - working_directory: - description: | - Directory containing `Cargo.toml` (relative to the repo root). All - cargo invocations cd into this directory; `hashFiles()` guards also - consult it. Default `.` keeps single-crate repos unchanged. Set - to e.g. `crates/server` for a sub-crate, or pass a different - value per wrapper call when running the reusable in a workspace - via separate jobs. - type: string - required: false - default: "." - zig_version: - description: | - Exact Zig version required by a Rust crate's native build. Leave - empty for pure-Rust workspaces. When set, check, test, and coverage - jobs install the same compiler before invoking Cargo. - type: string - required: false - default: "" - -# Only `contents: read` is requested. A reusable workflow may narrow the -# caller's permissions but never widen them: requesting a permission the -# caller has not granted aborts the run as `startup_failure` with ZERO -# jobs — no logs, no red step, just an empty run. The previous -# `actions: read` here was used by no job in this file, so every caller -# granting only `contents: read` (the estate default) failed to start. -permissions: - contents: read - -jobs: - # Skip the whole reusable when the repo has no Cargo.toml — lets consumers - # add the wrapper unconditionally without worrying about repos that don't - # ship Rust code yet. This MUST be a checked-out step, NOT a job-level - # `if: hashFiles(...)`: job `if:` is evaluated server-side before any - # checkout, so hashFiles() sees an empty workspace and always returns '' - # — which silently skipped every job on EVERY repo, Rust or not. The - # detect job checks out and exposes a real boolean the others gate on. - detect: - timeout-minutes: 5 - name: Detect Cargo.toml - runs-on: ${{ inputs.runs-on }} - permissions: - contents: read - outputs: - has_cargo: ${{ steps.detect.outputs.has_cargo }} - steps: - - name: Checkout repository - uses: actions/checkout@v7.0.1 - with: - repository: ${{ github.repository }} - ref: ${{ github.ref }} - - name: Detect Cargo.toml - id: detect - run: | - if [ -f "${{ inputs.working_directory }}/Cargo.toml" ]; then - echo "has_cargo=true" >> "$GITHUB_OUTPUT" - else - echo "has_cargo=false" >> "$GITHUB_OUTPUT" - fi - - check: - timeout-minutes: 20 - name: Cargo check + clippy + fmt - runs-on: ${{ inputs.runs-on }} - needs: detect - if: ${{ needs.detect.outputs.has_cargo == 'true' }} - permissions: - contents: read - defaults: - run: - working-directory: ${{ inputs.working_directory }} - steps: - - name: Checkout repository - uses: actions/checkout@v7.0.1 - with: - repository: ${{ github.repository }} - ref: ${{ github.ref }} - - - name: Install Rust toolchain - # `toolchain:` is mandatory because the action is pinned by commit SHA: - # dtolnay/rust-toolchain infers the toolchain from the `@`-ref (e.g. - # `@stable`), but a SHA ref carries no version, so the action's "parse - # toolchain version" step fails with `'toolchain' is a required input`. - # See standards estate-wide rust-ci red. - uses: dtolnay/rust-toolchain@v1 - with: - toolchain: stable - components: clippy, rustfmt - - - name: Install native schema compilers - run: | - sudo apt-get update - sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev - - - name: Install Zig for native build - if: ${{ inputs.zig_version != '' }} - uses: goto-bus-stop/setup-zig@v2.2.1 - with: - version: ${{ inputs.zig_version }} - - - name: Cache cargo registry and build - uses: Swatinem/rust-cache@v2.9.2 - with: - workspaces: ${{ inputs.working_directory }} - - - name: Cargo check - # `--locked` so CI honours `Cargo.lock` and surfaces dep drift the - # first push it happens, instead of silently re-resolving (which - # masked the echidna#92 / echidna PR #128 dependabot major-bump - # break for 24h). See standards#295. - run: cargo check --locked ${{ inputs.check_args }} - - - name: Cargo fmt - run: cargo fmt --all -- --check - - - name: Cargo clippy - run: cargo clippy --locked ${{ inputs.clippy_args }} - - test: - timeout-minutes: 20 - name: Cargo test - runs-on: ${{ inputs.runs-on }} - needs: [detect, check] - if: ${{ needs.detect.outputs.has_cargo == 'true' }} - permissions: - contents: read - defaults: - run: - working-directory: ${{ inputs.working_directory }} - steps: - - name: Checkout repository - uses: actions/checkout@v7.0.1 - with: - repository: ${{ github.repository }} - ref: ${{ github.ref }} - - - name: Install Rust toolchain - # `toolchain:` mandatory under SHA pin — see Cargo check job above. - uses: dtolnay/rust-toolchain@v1 - with: - toolchain: stable - - - name: Install native schema compilers - run: | - sudo apt-get update - sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev - - - name: Install Zig for native build - if: ${{ inputs.zig_version != '' }} - uses: goto-bus-stop/setup-zig@v2.2.1 - with: - version: ${{ inputs.zig_version }} - - - name: Cache cargo registry and build - uses: Swatinem/rust-cache@v2.9.2 - with: - workspaces: ${{ inputs.working_directory }} - - - name: Run tests - # `--locked` — see Cargo check above. - run: cargo test --locked ${{ inputs.test_args }} - - - name: Write summary - if: always() - run: | - { - echo "## Rust CI Results" - echo "" - echo "- **cargo check**: ${{ needs.check.result }}" - echo "- **cargo test**: completed" - } >> "$GITHUB_STEP_SUMMARY" - - audit: - timeout-minutes: 20 - name: Cargo audit (security) - runs-on: ${{ inputs.runs-on }} - needs: detect - if: ${{ inputs.enable_audit && needs.detect.outputs.has_cargo == 'true' }} - permissions: - contents: read - defaults: - run: - working-directory: ${{ inputs.working_directory }} - steps: - - name: Checkout repository - uses: actions/checkout@v7.0.1 - with: - repository: ${{ github.repository }} - ref: ${{ github.ref }} - - - name: Install Rust toolchain - # `toolchain:` mandatory under SHA pin — see Cargo check job above. - uses: dtolnay/rust-toolchain@v1 - with: - toolchain: stable - - - name: Install cargo-audit - # Use the binstall path when available to skip a from-source rebuild - # on every run — was the single biggest contributor to slow CI on - # repos that opted in to audit (~3–4 minute install). - run: cargo install cargo-audit --locked - - - name: Security audit - run: cargo audit - - coverage: - timeout-minutes: 25 - name: llvm-cov line coverage - runs-on: ${{ inputs.runs-on }} - needs: detect - if: ${{ inputs.enable_coverage && needs.detect.outputs.has_cargo == 'true' }} - permissions: - contents: read - defaults: - run: - working-directory: ${{ inputs.working_directory }} - env: - # Ratcheted line-coverage floor (from the caller). Raise toward target; never lower. - FLOOR: ${{ inputs.coverage_floor }} - steps: - - name: Checkout repository - uses: actions/checkout@v7.0.1 - with: - repository: ${{ github.repository }} - ref: ${{ github.ref }} - - - name: Install Rust toolchain - # `toolchain:` mandatory under SHA pin — see Cargo check job above. - uses: dtolnay/rust-toolchain@v1 - with: - toolchain: stable - components: llvm-tools-preview - - - name: Install native schema compilers - run: | - sudo apt-get update - sudo apt-get install -y capnproto protobuf-compiler pkg-config libssl-dev - - - name: Install Zig for native build - if: ${{ inputs.zig_version != '' }} - uses: goto-bus-stop/setup-zig@v2.2.1 - with: - version: ${{ inputs.zig_version }} - - - name: Install cargo-llvm-cov - run: cargo install cargo-llvm-cov --locked - - - name: Measure line coverage - id: cov - # Self-contained: no external coverage service. Own the gate on our runner. - run: | - set -euo pipefail - cargo llvm-cov --locked --json --output-path cov.json - PCT=$(jq -r '.data[0].totals.lines.percent' cov.json) - printf '### Line coverage: %.2f%% (floor %s%%)\n' "$PCT" "$FLOOR" >> "$GITHUB_STEP_SUMMARY" - echo "pct=$PCT" >> "$GITHUB_OUTPUT" - - - name: Enforce ratchet floor - run: | - set -euo pipefail - awk -v p="${{ steps.cov.outputs.pct }}" -v f="$FLOOR" 'BEGIN { - if (f !~ /^[0-9]+([.][0-9]+)?$/ || f + 0 > 100 || p !~ /^[0-9]+([.][0-9]+)?$/ || p + 0 > 100) { - print "FAIL: coverage and floor must be numeric percentages in [0, 100]"; exit 1 - } - if (p + 0 < f + 0) { printf "FAIL: line coverage %.2f%% is below floor %s%%\n", p, f; exit 1 } - printf "OK: line coverage %.2f%% >= floor %s%%\n", p, f - }' diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml new file mode 100644 index 00000000..30e75ac7 --- /dev/null +++ b/.github/workflows/static-analysis-gate.yml @@ -0,0 +1,466 @@ +# This workflow is managed by gh actions-lock. +# SPDX-License-Identifier: MPL-2.0 +# Static Analysis Gate — Required by branch protection rules. +# Runs panic-attack and hypatia, deposits findings for gitbot-fleet learning. +name: Static Analysis Gate +on: + pull_request: + branches: ['**'] + push: + branches: [main, master] +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +permissions: + contents: read +jobs: + # --------------------------------------------------------------------------- + # Job 1: panic-attack assail + # --------------------------------------------------------------------------- + panic-attack-assail: + name: panic-attack assail + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + fetch-depth: 0 + - name: Install panic-attack (if available) + id: install + run: | + # Try to fetch the latest release binary from the org + PA_URL="https://github.com/hyperpolymath/panic-attack/releases/latest/download/panic-attack-linux-x86_64" + if curl -fsSL --head "$PA_URL" >/dev/null 2>&1; then + curl -fsSL -o /usr/local/bin/panic-attack "$PA_URL" + chmod +x /usr/local/bin/panic-attack + echo "installed=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::panic-attack binary not available — skipping assail" + echo "installed=false" >> "$GITHUB_OUTPUT" + fi + - name: Run panic-attack assail + id: assail + if: steps.install.outputs.installed == 'true' + run: | + set +e + panic-attack assail --format json . > panic-attack-findings.json + PA_EXIT=$? + set -e + + # Same defect class as the Hypatia job below: `2>&1` folded the + # scanner's stderr into the JSON payload, so every jq parse failed, + # every count silently became 0 via `|| echo 0`, and "Fail on critical + # findings" could never fire on any input. Keep stderr on the log. + if [ ! -s panic-attack-findings.json ]; then + echo "[]" > panic-attack-findings.json + fi + + # Deliberately a WARNING, not a failure. panic-attack is a downloaded + # release binary whose exit-code and output contract are not verified + # here, and it has no confirmed --exit-zero equivalent, so we surface a + # malformed payload in the log rather than block on an unverified tool. + # Promote to `exit 1` (as the Hypatia job does) once that contract is + # confirmed -- see the follow-up issue linked from this PR. + if ! jq -e 'type == "array"' panic-attack-findings.json >/dev/null 2>&1; then + echo "::warning::panic-attack output is not a JSON array (exit ${PA_EXIT}); counts below are unreliable" + fi + + # Parse finding counts + TOTAL=$(jq '. | length' panic-attack-findings.json 2>/dev/null || echo 0) + CRITICAL=$(jq '[.[] | select(.severity == "critical")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + HIGH=$(jq '[.[] | select(.severity == "high")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + MEDIUM=$(jq '[.[] | select(.severity == "medium" or .severity == "warn")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + LOW=$(jq '[.[] | select(.severity == "low")] | length' panic-attack-findings.json 2>/dev/null || echo 0) + + echo "total=$TOTAL" >> "$GITHUB_OUTPUT" + echo "critical=$CRITICAL" >> "$GITHUB_OUTPUT" + echo "high=$HIGH" >> "$GITHUB_OUTPUT" + echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" + echo "low=$LOW" >> "$GITHUB_OUTPUT" + echo "exit_code=$PA_EXIT" >> "$GITHUB_OUTPUT" + - name: Emit check annotations + if: steps.install.outputs.installed == 'true' + run: | + # Convert JSON findings into GitHub Actions annotations + # Findings carry no `.message` (keys: action,file,line,reason,rule_module, + # severity,type), so every annotation read "null". `.file` is an absolute + # runner path, which GitHub cannot anchor to the diff, so it is made + # workspace-relative here. + # Annotations are cosmetic, but a malformed findings file is reported + # instead of being swallowed. + if jq -e 'type == "array"' panic-attack-findings.json >/dev/null 2>&1; then + jq -r --arg ws "$GITHUB_WORKSPACE" '.[] | select(.file != null) | + (.file | ltrimstr($ws + "/")) as $f | + (.reason // .message // .type // "finding") as $m | + if .severity == "critical" then + "::error file=\($f),line=\(.line // 1)::[panic-attack] \($m)" + elif .severity == "high" then + "::error file=\($f),line=\(.line // 1)::[panic-attack] \($m)" + else + "::warning file=\($f),line=\(.line // 1)::[panic-attack] \($m)" + end + ' panic-attack-findings.json + else + echo "::warning::panic-attack-findings.json is not a JSON array; no annotations emitted" + fi + - name: Write step summary + if: steps.install.outputs.installed == 'true' + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## panic-attack assail Results + + | Severity | Count | + |----------|-------| + | Critical | ${{ steps.assail.outputs.critical }} | + | High | ${{ steps.assail.outputs.high }} | + | Medium | ${{ steps.assail.outputs.medium }} | + | Low | ${{ steps.assail.outputs.low }} | + | **Total**| ${{ steps.assail.outputs.total }} | + EOF + - name: Create stub findings (when panic-attack unavailable) + if: steps.install.outputs.installed != 'true' + run: | + echo "[]" > panic-attack-findings.json + echo "## panic-attack assail" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" + - name: Upload panic-attack findings + uses: actions/upload-artifact@v7.0.1 + with: + name: panic-attack-findings + path: panic-attack-findings.json + retention-days: 90 + - name: Fail on critical findings + if: steps.install.outputs.installed == 'true' && steps.assail.outputs.critical > 0 + run: | + echo "::error::panic-attack found ${{ steps.assail.outputs.critical }} critical issue(s) — blocking merge" + exit 1 + # --------------------------------------------------------------------------- + # Job 2: hypatia-scan + # + # NOTE — this is NOT a duplicate of the standalone `hypatia-scan.yml`. + # * THIS job runs Hypatia inside the gate and hands its findings to the + # `deposit-findings` job below, which feeds the gitbot-fleet LEARNING + # pipeline (artifact -> fleet). It is a REQUIRED status check. + # * `hypatia-scan.yml` runs Hypatia standalone as the repo's security scan, + # independent of the fleet-learning deposit. + # Same tool, two different consumers — keep both. See .github/workflows/README.adoc. + # --------------------------------------------------------------------------- + hypatia-scan: + name: Hypatia neurosymbolic scan + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + fetch-depth: 0 + - name: Setup Elixir for Hypatia scanner + id: beam + continue-on-error: true + uses: erlef/setup-beam@v1.24.1 + with: + elixir-version: '1.19.4' + otp-version: '28.3' + - name: Clone and build Hypatia + id: build + continue-on-error: true + run: | + git clone https://github.com/hyperpolymath/hypatia.git "$HOME/hypatia" 2>/dev/null || true + if [ -f "$HOME/hypatia/mix.exs" ]; then + cd "$HOME/hypatia" + # Build escript if neither hypatia nor hypatia-v2 exists + if [ ! -f hypatia ] && [ ! -f hypatia-v2 ]; then + mix deps.get + mix escript.build + fi + echo "ready=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::Hypatia scanner not available — skipping scan" + echo "ready=false" >> "$GITHUB_OUTPUT" + fi + - name: Run Hypatia scan + id: scan + if: steps.build.outputs.ready == 'true' + run: | + set +e + HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . --exit-zero > hypatia-findings.json + HYP_EXIT=$? + set -e + + # --exit-zero is Hypatia's own documented CI recipe (lib/hypatia/cli.ex), + # for exactly this case: "use in CI when a downstream step gates on + # severity counts". Findings go to stdout, the one-line summary to + # stderr, and the process exits 0 unless the SCANNER itself failed. + # + # Do NOT redirect stderr into the payload with `2>&1`: that folds the + # summary line into the JSON, so every parse fails, the old `[]` + # fallback substituted a clean result, CRITICAL was always 0, and the + # gate below could never fire on any input. Keep stderr on the log. + if [ "$HYP_EXIT" -ne 0 ]; then + echo "::error::Hypatia scanner execution failed with exit ${HYP_EXIT}" + exit "$HYP_EXIT" + fi + # `jq empty` is NOT sufficient -- it succeeds on any valid JSON, + # including a bare string, object or null. Assert the array. + if [ ! -s hypatia-findings.json ] || ! jq -e 'type == "array"' hypatia-findings.json >/dev/null; then + echo "::error::Hypatia did not produce a valid JSON findings array" + exit 1 + fi + + TOTAL=$(jq '. | length' hypatia-findings.json 2>/dev/null || echo 0) + CRITICAL=$(jq '[.[] | select(.severity == "critical")] | length' hypatia-findings.json 2>/dev/null || echo 0) + HIGH=$(jq '[.[] | select(.severity == "high")] | length' hypatia-findings.json 2>/dev/null || echo 0) + MEDIUM=$(jq '[.[] | select(.severity == "medium" or .severity == "warn")] | length' hypatia-findings.json 2>/dev/null || echo 0) + LOW=$(jq '[.[] | select(.severity == "low")] | length' hypatia-findings.json 2>/dev/null || echo 0) + + echo "total=$TOTAL" >> "$GITHUB_OUTPUT" + echo "critical=$CRITICAL" >> "$GITHUB_OUTPUT" + echo "high=$HIGH" >> "$GITHUB_OUTPUT" + echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" + echo "low=$LOW" >> "$GITHUB_OUTPUT" + - name: Emit check annotations + if: steps.build.outputs.ready == 'true' + run: | + # Findings carry no `.message` (keys: action,file,line,reason,rule_module, + # severity,type), so every annotation read "null". `.file` is an absolute + # runner path, which GitHub cannot anchor to the diff, so it is made + # workspace-relative here. + # Annotations are cosmetic, but a malformed findings file is reported + # instead of being swallowed. + if jq -e 'type == "array"' hypatia-findings.json >/dev/null 2>&1; then + jq -r --arg ws "$GITHUB_WORKSPACE" '.[] | select(.file != null) | + (.file | ltrimstr($ws + "/")) as $f | + (.reason // .message // .type // "finding") as $m | + if .severity == "critical" then + "::error file=\($f),line=\(.line // 1)::[hypatia] \($m)" + elif .severity == "high" then + "::error file=\($f),line=\(.line // 1)::[hypatia] \($m)" + else + "::warning file=\($f),line=\(.line // 1)::[hypatia] \($m)" + end + ' hypatia-findings.json + else + echo "::warning::hypatia-findings.json is not a JSON array; no annotations emitted" + fi + - name: Write step summary + if: steps.build.outputs.ready == 'true' + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## Hypatia Scan Results + + | Severity | Count | + |----------|-------| + | Critical | ${{ steps.scan.outputs.critical }} | + | High | ${{ steps.scan.outputs.high }} | + | Medium | ${{ steps.scan.outputs.medium }} | + | Low | ${{ steps.scan.outputs.low }} | + | **Total**| ${{ steps.scan.outputs.total }} | + EOF + - name: Create stub findings (when Hypatia unavailable) + if: steps.build.outputs.ready != 'true' + run: | + echo "[]" > hypatia-findings.json + echo "## Hypatia Scan" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + echo "Skipped: Hypatia scanner not available in this environment." >> "$GITHUB_STEP_SUMMARY" + - name: Upload hypatia findings + uses: actions/upload-artifact@v7.0.1 + with: + name: hypatia-findings + path: hypatia-findings.json + retention-days: 90 + - name: Fail on critical security findings + if: steps.build.outputs.ready == 'true' && steps.scan.outputs.critical > 0 + run: | + echo "::error::Hypatia found ${{ steps.scan.outputs.critical }} critical security issue(s) — blocking merge" + exit 1 + # --------------------------------------------------------------------------- + # Job 3: patch-bridge triage (CVE contextual assessment) + # --------------------------------------------------------------------------- + patch-bridge-triage: + name: Patch Bridge CVE triage + runs-on: ubuntu-24.04 + timeout-minutes: 15 + steps: + - name: Checkout repository + uses: actions/checkout@v7.0.1 + with: + fetch-depth: 0 + - name: Install panic-attack (if available) + id: install + run: | + PA_URL="https://github.com/hyperpolymath/panic-attack/releases/latest/download/panic-attack-linux-x86_64" + if curl -fsSL --head "$PA_URL" >/dev/null 2>&1; then + curl -fsSL -o /usr/local/bin/panic-attack "$PA_URL" + chmod +x /usr/local/bin/panic-attack + echo "installed=true" >> "$GITHUB_OUTPUT" + else + echo "::notice::panic-attack binary not available — skipping Patch Bridge" + echo "installed=false" >> "$GITHUB_OUTPUT" + fi + - name: Run Patch Bridge triage + id: triage + if: steps.install.outputs.installed == 'true' + run: | + set +e + panic-attack bridge triage --format json . > bridge-report.json 2>&1 + PB_EXIT=$? + set -e + + if [ ! -s bridge-report.json ] || ! jq empty bridge-report.json 2>/dev/null; then + echo '{"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > bridge-report.json + fi + + UNMITIGABLE=$(jq '.unmitigable // 0' bridge-report.json) + MITIGATED=$(jq '.mitigated // 0' bridge-report.json) + CONCATENATIVE=$(jq '.concatenative // 0' bridge-report.json) + INFORMATIONAL=$(jq '.informational // 0' bridge-report.json) + + echo "unmitigable=$UNMITIGABLE" >> "$GITHUB_OUTPUT" + echo "mitigated=$MITIGATED" >> "$GITHUB_OUTPUT" + echo "concatenative=$CONCATENATIVE" >> "$GITHUB_OUTPUT" + echo "informational=$INFORMATIONAL" >> "$GITHUB_OUTPUT" + - name: Write step summary + if: steps.install.outputs.installed == 'true' + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## Patch Bridge CVE Triage + + | Classification | Count | + |----------------|-------| + | Unmitigable | ${{ steps.triage.outputs.unmitigable }} | + | Mitigated | ${{ steps.triage.outputs.mitigated }} | + | Concatenative | ${{ steps.triage.outputs.concatenative }} | + | Informational | ${{ steps.triage.outputs.informational }} | + + Unmitigable CVEs require dependency replacement or rearchitecture. + Mitigated CVEs have active controls with soundness proofs. + Concatenative risks are CVE combinations that multiply severity. + EOF + - name: Create stub report (when unavailable) + if: steps.install.outputs.installed != 'true' + run: | + echo '{"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > bridge-report.json + echo "## Patch Bridge CVE Triage" >> "$GITHUB_STEP_SUMMARY" + echo "" >> "$GITHUB_STEP_SUMMARY" + echo "Skipped: panic-attack not available in this environment." >> "$GITHUB_STEP_SUMMARY" + - name: Upload bridge report + uses: actions/upload-artifact@v7.0.1 + with: + name: bridge-report + path: bridge-report.json + retention-days: 90 + - name: Fail on unmitigable CVEs in critical paths + if: steps.install.outputs.installed == 'true' && steps.triage.outputs.unmitigable > 0 + run: | + echo "::warning::Patch Bridge found ${{ steps.triage.outputs.unmitigable }} unmitigable CVE(s) — review required" + # Warning only, not blocking. Unmitigable means the developer needs + # to make an architectural decision, not that the PR is wrong. + # --------------------------------------------------------------------------- + # Job 4: deposit-findings (combines + archives for gitbot-fleet) + # --------------------------------------------------------------------------- + deposit-findings: + name: Deposit findings for gitbot-fleet + runs-on: ubuntu-24.04 + timeout-minutes: 15 + needs: [panic-attack-assail, hypatia-scan, patch-bridge-triage] + if: always() + steps: + - name: Download panic-attack findings + uses: actions/download-artifact@v8.0.1 + with: + name: panic-attack-findings + path: findings/ + - name: Download hypatia findings + uses: actions/download-artifact@v8.0.1 + with: + name: hypatia-findings + path: findings/ + - name: Download bridge report + uses: actions/download-artifact@v8.0.1 + with: + name: bridge-report + path: findings/ + - name: Combine findings into unified report + id: combine + run: | + PA_FILE="findings/panic-attack-findings.json" + HYP_FILE="findings/hypatia-findings.json" + + # Ensure both files exist and are valid JSON arrays + for f in "$PA_FILE" "$HYP_FILE"; do + if [ ! -s "$f" ] || ! jq empty "$f" 2>/dev/null; then + echo "[]" > "$f" + fi + done + + # Tag each finding with its source scanner + jq '[.[] | . + {"scanner": "panic-attack"}]' "$PA_FILE" > /tmp/pa-tagged.json + jq '[.[] | . + {"scanner": "hypatia"}]' "$HYP_FILE" > /tmp/hyp-tagged.json + + # Read bridge report (CVE triage, not findings array) + BRIDGE_FILE="findings/bridge-report.json" + if [ ! -s "$BRIDGE_FILE" ] || ! jq empty "$BRIDGE_FILE" 2>/dev/null; then + echo '{"cves":[],"mitigated":0,"unmitigable":0,"concatenative":0,"informational":0}' > "$BRIDGE_FILE" + fi + + # Build unified report envelope + jq -n \ + --arg repo "${{ github.repository }}" \ + --arg sha "${{ github.sha }}" \ + --arg ref "${{ github.ref }}" \ + --arg run_id "${{ github.run_id }}" \ + --arg ts "$(date -u +%Y-%m-%dT%H:%M:%SZ)" \ + --slurpfile pa /tmp/pa-tagged.json \ + --slurpfile hyp /tmp/hyp-tagged.json \ + --slurpfile bridge "$BRIDGE_FILE" \ + '{ + schema_version: "1.1.0", + repository: $repo, + commit_sha: $sha, + ref: $ref, + run_id: $run_id, + timestamp: $ts, + findings: ($pa[0] + $hyp[0]), + patch_bridge: $bridge[0] + }' > findings/unified-findings.json + + TOTAL=$(jq '.findings | length' findings/unified-findings.json) + CRITICAL=$(jq '[.findings[] | select(.severity == "critical")] | length' findings/unified-findings.json) + HIGH=$(jq '[.findings[] | select(.severity == "high")] | length' findings/unified-findings.json) + MEDIUM=$(jq '[.findings[] | select(.severity == "medium" or .severity == "warn")] | length' findings/unified-findings.json) + LOW=$(jq '[.findings[] | select(.severity == "low")] | length' findings/unified-findings.json) + + echo "total=$TOTAL" >> "$GITHUB_OUTPUT" + echo "critical=$CRITICAL" >> "$GITHUB_OUTPUT" + echo "high=$HIGH" >> "$GITHUB_OUTPUT" + echo "medium=$MEDIUM" >> "$GITHUB_OUTPUT" + echo "low=$LOW" >> "$GITHUB_OUTPUT" + - name: Upload unified findings (fleet scanner picks these up) + uses: actions/upload-artifact@v7.0.1 + with: + name: unified-findings + path: findings/unified-findings.json + retention-days: 90 + - name: Write deposit summary + run: | + cat <> "$GITHUB_STEP_SUMMARY" + ## Unified Findings Deposit + + **Repository:** ${{ github.repository }} + **Commit:** \`${{ github.sha }}\` + **Deposited at:** $(date -u +"%Y-%m-%d %H:%M:%S UTC") + + | Severity | Count | + |----------|-------| + | Critical | ${{ steps.combine.outputs.critical }} | + | High | ${{ steps.combine.outputs.high }} | + | Medium | ${{ steps.combine.outputs.medium }} | + | Low | ${{ steps.combine.outputs.low }} | + | **Total**| ${{ steps.combine.outputs.total }} | + + Findings saved as \`unified-findings\` artifact. + The gitbot-fleet scanner will ingest these on its next pass. + EOF diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml deleted file mode 100644 index 100f21f2..00000000 --- a/.gitlab-ci.yml +++ /dev/null @@ -1,299 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors -# -# ECHIDNA GitLab CI/CD Pipeline -# Comprehensive build, test, quality check, and deploy stages - -workflow: - rules: - - if: $CI_PIPELINE_SOURCE == "merge_request_event" - - if: $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH - - if: $CI_COMMIT_TAG - -variables: - CARGO_HOME: "${CI_PROJECT_DIR}/.cargo" - RUST_BACKTRACE: "1" - JULIA_DEPOT_PATH: "${CI_PROJECT_DIR}/.julia" - PODMAN_BUILDAH_ISOLATION: "chroot" - -stages: - - lint - - build - - test - - quality - - security - - deploy - -# ============================================================================= -# Cache Configuration -# ============================================================================= -.rust_cache: - cache: - key: rust-${CI_COMMIT_REF_SLUG} - paths: - - .cargo/ - - target/ - -.julia_cache: - cache: - key: julia-${CI_COMMIT_REF_SLUG} - paths: - - .julia/ - -# ============================================================================= -# Stage 1: Linting and Formatting -# ============================================================================= - -reuse-lint: - stage: lint - image: docker.io/fsfe/reuse:latest - script: - - reuse lint - allow_failure: false - -rust-fmt: - stage: lint - image: docker.io/library/rust:1.75-slim - extends: .rust_cache - script: - - rustup component add rustfmt - - cargo fmt -- --check - allow_failure: false - -rust-clippy: - stage: lint - image: docker.io/library/rust:1.75-slim - extends: .rust_cache - before_script: - - apt-get update && apt-get install -y pkg-config libssl-dev - - rustup component add clippy - script: - - cargo clippy --all-targets --all-features -- -D warnings - allow_failure: false - -# ============================================================================= -# Stage 2: Build -# ============================================================================= - -build-rust: - stage: build - image: docker.io/library/rust:1.75-slim - extends: .rust_cache - before_script: - - apt-get update && apt-get install -y pkg-config libssl-dev build-essential - script: - - cargo build --release - artifacts: - paths: - - target/release/echidna* - expire_in: 1 day - -build-julia: - stage: build - image: docker.io/library/julia:1.10 - extends: .julia_cache - script: - - julia --project=. -e 'using Pkg; Pkg.instantiate(); Pkg.precompile()' - artifacts: - paths: - - Manifest.toml - - .julia/ - expire_in: 1 day - - -build-container: - stage: build - image: quay.io/podman/stable:latest - services: - - name: docker:dind - command: ["--tls=false"] - variables: - DOCKER_HOST: tcp://docker:2375 - before_script: - - podman --version - script: - - podman build -f Containerfile -t echidna:${CI_COMMIT_SHORT_SHA} . - - podman save echidna:${CI_COMMIT_SHORT_SHA} -o echidna-image.tar - artifacts: - paths: - - echidna-image.tar - expire_in: 1 day - only: - - main - - merge_requests - - tags - -# ============================================================================= -# Stage 3: Testing -# ============================================================================= - -test-rust: - stage: test - image: docker.io/library/rust:1.75-slim - extends: .rust_cache - before_script: - - apt-get update && apt-get install -y pkg-config libssl-dev build-essential - script: - - cargo test --all-features --verbose - coverage: '/^\s*lines\.+:\s+(\d+\.\d+)%/' - artifacts: - reports: - coverage_report: - coverage_format: cobertura - path: coverage.xml - expire_in: 30 days - -test-julia: - stage: test - image: docker.io/library/julia:1.10 - extends: .julia_cache - script: - - julia --project=. -e 'using Pkg; Pkg.test(coverage=true)' - - julia --project=. -e 'using Coverage; coverage = process_folder(); covered_lines, total_lines = get_summary(coverage); println("Coverage: ", covered_lines/total_lines*100, "%")' - coverage: '/Coverage: \d+\.\d+/' - -test-integration: - stage: test - image: docker.io/library/rust:1.75-slim - extends: .rust_cache - before_script: - - apt-get update && apt-get install -y pkg-config libssl-dev build-essential z3 cvc5 - script: - - cargo test --test integration_tests --verbose - allow_failure: true - -# ============================================================================= -# Stage 4: Quality Checks -# ============================================================================= - -quality-aqua: - stage: quality - image: docker.io/library/julia:1.10 - extends: .julia_cache - script: - - julia --project=. -e 'using Pkg; Pkg.add("Aqua"); using Aqua; Aqua.test_all()' - allow_failure: true - -quality-jet: - stage: quality - image: docker.io/library/julia:1.10 - extends: .julia_cache - script: - - julia --project=. -e 'using Pkg; Pkg.add("JET"); using JET; report_file()' - allow_failure: true - -quality-coverage: - stage: quality - image: docker.io/library/julia:1.10 - extends: .julia_cache - script: - - julia --project=. -e 'using Pkg; Pkg.add("Coverage"); using Coverage; coverage = process_folder(); LCOV.writefile("coverage.info", coverage)' - artifacts: - paths: - - coverage.info - expire_in: 30 days - allow_failure: true - -# ============================================================================= -# Stage 5: Security Scanning -# ============================================================================= - -security-trivy-fs: - stage: security - image: docker.io/aquasec/trivy:latest - script: - - trivy fs --exit-code 0 --severity HIGH,CRITICAL --format table . - - trivy fs --exit-code 1 --severity CRITICAL --format json -o trivy-fs-report.json . - artifacts: - paths: - - trivy-fs-report.json - expire_in: 30 days - allow_failure: true - -security-trivy-container: - stage: security - image: docker.io/aquasec/trivy:latest - dependencies: - - build-container - before_script: - - apk add --no-cache podman - script: - - podman load -i echidna-image.tar - - trivy image --exit-code 0 --severity HIGH,CRITICAL echidna:${CI_COMMIT_SHORT_SHA} - - trivy image --exit-code 1 --severity CRITICAL --format json -o trivy-image-report.json echidna:${CI_COMMIT_SHORT_SHA} - artifacts: - paths: - - trivy-image-report.json - expire_in: 30 days - allow_failure: true - only: - - main - - merge_requests - - tags - -security-cargo-audit: - stage: security - image: docker.io/library/rust:1.75-slim - script: - - cargo install cargo-audit - - cargo audit - allow_failure: true - -# ============================================================================= -# Stage 6: Deployment -# ============================================================================= - -deploy-docs: - stage: deploy - image: docker.io/library/ruby:3.2 - script: - - echo "Deploying documentation..." - - mkdir -p public - - cp -r docs/* public/ - artifacts: - paths: - - public - only: - - main - -deploy-container-registry: - stage: deploy - image: quay.io/podman/stable:latest - services: - - name: docker:dind - command: ["--tls=false"] - variables: - DOCKER_HOST: tcp://docker:2375 - dependencies: - - build-container - before_script: - - echo "${CI_REGISTRY_PASSWORD}" | podman login -u "${CI_REGISTRY_USER}" --password-stdin "${CI_REGISTRY}" - script: - - podman load -i echidna-image.tar - - podman tag echidna:${CI_COMMIT_SHORT_SHA} ${CI_REGISTRY_IMAGE}:${CI_COMMIT_TAG} - - podman tag echidna:${CI_COMMIT_SHORT_SHA} ${CI_REGISTRY_IMAGE}:latest - - podman push ${CI_REGISTRY_IMAGE}:${CI_COMMIT_TAG} - - podman push ${CI_REGISTRY_IMAGE}:latest - only: - - tags - -deploy-release: - stage: deploy - image: registry.gitlab.com/gitlab-org/release-cli:latest - script: - - echo "Creating GitLab Release..." - release: - tag_name: ${CI_COMMIT_TAG} - description: "ECHIDNA Release ${CI_COMMIT_TAG}" - assets: - links: - - name: "Container Image" - url: "${CI_REGISTRY_IMAGE}:${CI_COMMIT_TAG}" - only: - - tags - -trufflehog: - stage: security - image: trufflesecurity/trufflehog:latest - script: - - trufflehog git file://. --only-verified --fail diff --git a/.hypatia-baseline.json b/.hypatia-baseline.json index 906ccf17..693f097d 100644 --- a/.hypatia-baseline.json +++ b/.hypatia-baseline.json @@ -1,2158 +1,539 @@ [ - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/BojForeign.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/CoprocessorForeign.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/EchidnaABI/AxiomTracker.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/EchidnaABI/CapnSchemas.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/EchidnaABI/Gnn.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/Layout.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/Overlay.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/OverlayForeign.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/TentaclesForeign.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/TypeLLForeign.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "src/abi/Types.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/AxiomCompleteness.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/AxiomPolicyOrdering.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/ClampTrustBounds.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/ProofStateSerialisation.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/TrustKernelMonotonicity.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "believe_me", - "file": "verification/proofs/idris2/TrustLevelSoundness.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "sorry", - "file": "verification/proofs/lean4/ParetoMaximality.lean" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unsafe_perform_io", - "file": "verification/proofs/idris2/AxiomCompleteness.idr" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "crates/echidna-core-spark/src/axiom_tracker.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/interfaces/graphql/schema.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/agent/meta_controller.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/agent/swarm.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/coprocessor/graphics.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/corpus/metrics.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/diagnostics/corpus_monitor.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/exchange/dedukti.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/gnn/client.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/gnn/embeddings.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/gnn/graph.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/learning/design_search.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/provers/agda.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/provers/isabelle.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/repl/proof.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/server.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/suggest/extractor.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/vcl_ut.rs" - }, - { - "severity": "critical", - "rule_module": "code_safety", - "type": "unwrap_dangerous_default", - "file": "src/rust/verisim_bridge.rs" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Boj/Foreign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/BojForeign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/CoprocessorForeign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/EchidnaABI/AxiomTracker.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/EchidnaABI/CapnSchemas.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/EchidnaABI/Gnn.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/EchidnaABI/Layout.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/EchidnaABI/Types.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Layout.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Overlay.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Overlay/Foreign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/OverlayForeign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Tentacles/Foreign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/TentaclesForeign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/TypeLL/Foreign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/TypeLLForeign.idr" - }, - { - "severity": "critical", - "rule_module": "structural_drift", - "type": "SD008", - "file": "src/abi/Types.idr" - }, - { - "severity": "critical", - "rule_module": "workflow_audit", - "type": "actions_expression_injection", - "file": "boj-build.yml" - }, - { - "severity": "critical", - "rule_module": "workflow_audit", - "type": "actions_expression_injection", - "file": "ghcr-publish.yml" - }, - { - "severity": "critical", - "rule_module": "workflow_audit", - "type": "actions_expression_injection", - "file": "hypatia-scan.yml" - }, - { - "severity": "critical", - "rule_module": "workflow_audit", - "type": "actions_expression_injection", - "file": "mirror.yml" - }, - { - "severity": "critical", - "rule_module": "workflow_audit", - "type": "actions_expression_injection", - "file": "quality.yml" - }, - { - "severity": "high", - "rule_module": "cicd_rules", - "type": "missing_requirement", - "file": ".github/dependabot.yml" - }, - { - "severity": "high", - "rule_module": "cicd_rules", - "type": "missing_requirement", - "file": ".github/workflows/scorecard.yml" - }, - { - "severity": "high", - "rule_module": "cicd_rules", - "type": "missing_requirement", - "file": "permissions: read-all" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "assert_smaller", - "file": "verification/proofs/idris2/AxiomCompleteness.idr" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "assert_total", - "file": "verification/proofs/idris2/AxiomCompleteness.idr" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "assert_total", - "file": "verification/proofs/idris2/ProofStateSerialisation.idr" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "from_raw", - "file": "src/rust/ffi/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "from_raw", - "file": "src/rust/provers/opensmt.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/dispatch.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/fault_tolerance/resilience.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "lock_unwrap", - "file": "src/rust/provers/lean.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "mem_forget", - "file": "src/rust/ffi/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/audio.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/crypto.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/dsp.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/flint.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/fpga.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/graphics.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/io.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/math.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/parigp.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/physics.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/tensor.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/coprocessor/vector.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/diagnostics/corpus_monitor.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/disciplines/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/exchange/dedukti.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/ffi/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/learning/self_play.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/abc.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/acl2.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/agda.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/cadical.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/dreal.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/hol4.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/idris2.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/isabelle.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/key.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/keymaerax.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/metamath.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/outcome.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/proverif.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/pvs.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/seahorn.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/vampire.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/viper.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/provers/z3.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "src/rust/verification/axiom_tracker.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/aspect_tests.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/common/assertions.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/integration_v1_2.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/live_prover_suite.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/live_prover_verify.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "panic_macro", - "file": "tests/sanity_suite.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unimplemented_macro", - "file": "src/rust/coprocessor/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "benches/proof_benchmarks.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "benches/routing_benchmarks.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "crates/echidna-core/src/types.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "crates/echidna-wire/src/lib.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "crates/typed_wasm/src/lib.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/interfaces/graphql/main.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/interfaces/graphql/schema.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/interfaces/rest/main.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/agent/actors.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/agent/memory.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/agent/planner.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/audio.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/crypto.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/dsp.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/flint.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/fpga.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/gap.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/graphics.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/io.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/macaulay2.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/math.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/maxima.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/parigp.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/physics.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/singular.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/tensor.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/coprocessor/vector.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/corpus/agda.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/corpus/coq.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/corpus/idris2.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/corpus/lean.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/corpus/octad.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/diagnostics/corpus_monitor.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/diagnostics/gnn_training.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/dispatch.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/exchange/dedukti.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/exchange/opentheory.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/fault_tolerance/resilience.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/ffi/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/gnn/graph.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/groove.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/integration.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/integrations/conceptnet.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/integrity/io.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/ipc/mod.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/learning/self_play.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/proof_encoding.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/proof_search.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/abc.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/abella.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/agda.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/agsyhol.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/alloy.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/altergo.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/cadical.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/cameleer.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/cbmc.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/chuffed.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/coq.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/cubical_agda.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/cvc5.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/dafny.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/dedukti.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/dreal.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/easycrypt.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/eprover.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/faial.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/framac.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/fstar.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/glpk.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/gnatprove.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/gpuverify.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/imandra.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/io.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/key.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/keymaerax.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/kissat.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/lash.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/lean.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/lean3.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/leo3.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/liquid_haskell.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/metamath.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/minisat.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/minizinc.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/minlog.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/mizar.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/mizar_ar.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/nuprl.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/nusmv.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/opensmt.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/ortools.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/outcome.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/prism.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/prover9.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/proverif.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/rocq.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/satallax.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/scip.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/seahorn.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/smtrat.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/spass.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/spin_checker.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/stainless.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/tamarin.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/tlaps.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/tlc.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/tptp_output.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/twelf.rs" - }, - { - "severity": "high", - "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/typed_wasm.rs" - }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/uppaal.rs" + "type": "from_raw", + "file": "src/rust/ffi/mod.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/uppaal_stratego.rs" + "type": "from_raw", + "file": "src/rust/provers/opensmt.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/vampire.rs" + "type": "lock_unwrap", + "file": "src/rust/dispatch.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/viper.rs" + "type": "lock_unwrap", + "file": "src/rust/fault_tolerance/resilience.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/why3.rs" + "type": "lock_unwrap", + "file": "src/rust/provers/lean.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/provers/zipperposition.rs" + "type": "mem_forget", + "file": "src/rust/ffi/mod.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", - "type": "unwrap_without_check", - "file": "src/rust/repl/diagnostics.rs" + "type": "panic_macro", + "file": "src/rust/verification/axiom_tracker.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/repl/proof.rs" + "file": "crates/typed_wasm/src/lib.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/server.rs" + "file": "src/interfaces/graphql/schema.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/suggest/mod.rs" + "file": "src/rust/agent/actors.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/vcl_ut.rs" + "file": "src/rust/coprocessor/graphics.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/verification/certificates.rs" + "file": "src/rust/coprocessor/macaulay2.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/verification/portfolio.rs" + "file": "src/rust/coprocessor/maxima.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/verification/proof.rs" + "file": "src/rust/coprocessor/parigp.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/verification/statistics.rs" + "file": "src/rust/coprocessor/singular.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "src/rust/verisim_bridge.rs" + "file": "src/rust/dispatch.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/agentic_integration.rs" + "file": "src/rust/fault_tolerance/resilience.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/common/generators.rs" + "file": "src/rust/ipc/mod.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/common/mod.rs" + "file": "src/rust/proof_search.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/e2e_proof_pipeline.rs" + "file": "src/rust/provers/coq.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/e2e_prover_test.rs" + "file": "src/rust/provers/framac.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/full_health_system_test.rs" + "file": "src/rust/provers/lean.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/property_tests.rs" + "file": "src/rust/provers/mizar.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/sanity_suite.rs" + "file": "src/rust/repl/diagnostics.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/security_aspect_tests.rs" + "file": "src/rust/repl/proof.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/test_agda_backend.rs" + "file": "src/rust/server.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "high", "rule_module": "code_safety", "type": "unwrap_without_check", - "file": "tests/typed_wasm_properties.rs" - }, - { - "severity": "high", - "rule_module": "git_state", - "type": "GS005", - "file": "." - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/Components.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/Page.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/PlaygroundServer.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/Server.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/LeanTool.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Metamath.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/SystemOnTptp.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Unified.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/UnifiedTest.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Wolfram.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Z3Wasm.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/runners/Cli.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/runners/Daemon.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/types/Prover.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/types/ProverTest.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/utils/Http.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/Main.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/api/Client.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/GoalList.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/ProofTree.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/ProofViewer.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/ProverSelector.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/TacticSuggester.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/TheoremSearch.res" - }, - { - "severity": "high", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/state/Store.res" - }, - { - "severity": "high", - "rule_module": "workflow_audit", - "type": "download_then_run", - "file": "mirror.yml" - }, - { - "severity": "high", - "rule_module": "workflow_audit", - "type": "missing_workflow", - "file": "quality.yml" - }, - { - "severity": "high", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "security-scan.yml" - }, - { - "severity": "high", - "rule_module": "workflow_audit", - "type": "unsafe_curl_payload", - "file": "boj-build.yml" - }, - { - "severity": "high", - "rule_module": "workflow_audit", - "type": "unsafe_curl_payload", - "file": "hypatia-scan.yml" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/runners/Daemon.res", - "note": "AffineScript Belt/Js.* migration pending; hypatia now emits these at medium (baseline had high)" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/runners/Cli.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Wolfram.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/UnifiedTest.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/SystemOnTptp.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/LeanTool.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Z3Wasm.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Metamath.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/clients/Unified.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/types/Prover.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/types/ProverTest.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/provers/utils/Http.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/TheoremSearch.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/components/ProofTree.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/api/Client.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "src/affinescript/src/Main.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/JsCoq.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/Deno.res", - "note": "AffineScript Belt/Js.* migration pending" - }, - { - "severity": "medium", - "rule_module": "migration_rules", - "type": "deprecated_api", - "file": "echidna-playground/src/Dom.res", - "note": "AffineScript Belt/Js.* migration pending" + "file": "src/rust/verification/portfolio.rs", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/learning/design_search.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/provers/z3.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/coprocessor/julia_bridge.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/coprocessor/math.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/gnn/client.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/llm.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/neural.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/rust/corpus/octad.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "expect_in_hot_path", "file": "src/interfaces/graphql/resolvers.rs", - "note": "expect() triage tracked with existing unwrap_without_check debt" + "note": "expect() triage tracked with existing unwrap_without_check debt", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/rust/ffi/mod.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/rust/ffi/spark_axiom.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/rust/coprocessor/flint.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/rust/proof_search.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/interfaces/grpc/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/interfaces/rest/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "unsafe_block", "file": "src/interfaces/graphql/ffi_wrapper.rs", - "note": "FFI boundary; SAFETY-comment sweep pending" + "note": "FFI boundary; SAFETY-comment sweep pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/rust/ffi/mod.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/rust/ffi/spark_axiom.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/rust/coprocessor/flint.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/rust/proof_search.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/interfaces/grpc/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/interfaces/rest/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "code_safety", "type": "as_ptr", "file": "src/interfaces/graphql/ffi_wrapper.rs", - "note": "FFI boundary; pointer-lifetime audit pending" + "note": "FFI boundary; pointer-lifetime audit pending", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "structural_drift", "type": "SD022", "file": ".machine_readable/descriptiles/STATE.a2ml", - "note": "Paths cited are in EXTERNAL corpora repos (mirror-isabelle, viperproject/silver, vcl-ut), not this tree; SD022 cannot see that" + "note": "Paths cited are in EXTERNAL corpora repos (mirror-isabelle, viperproject/silver, vcl-ut), not this tree; SD022 cannot see that", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "structural_drift", "type": "SD022", "file": "docs/SSG_ROADMAP.adoc", - "note": "Roadmap doc: paths are planned future modules, not renames" - }, - { - "severity": "medium", - "rule_module": "scorecard", - "type": "DependencyPinning", - "file": "." - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "agda-meta-checker.yml" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "boj-build.yml" - }, - { - "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "bridge-gate.yml" + "note": "Roadmap doc: paths are planned future modules, not renames", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "workflow_audit", "type": "unpinned_action", - "file": "cargo-audit.yml" + "file": "agda-meta-checker.yml", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "workflow_audit", "type": "unpinned_action", - "file": "cflite_batch.yml" + "file": "codeql.yml", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "workflow_audit", "type": "unpinned_action", - "file": "cflite_pr.yml" + "file": "mvp-smoke.yml", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", "rule_module": "workflow_audit", "type": "unpinned_action", - "file": "chapel-ci.yml" + "file": "s4-loop.yml", + "tracking_issue": "hyperpolymath/echidna#314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "codeql.yml" + "rule_module": "research_extensions", + "type": "RE001", + "file": ".github/workflows/labels.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "container-ci.yml" + "rule_module": "research_extensions", + "type": "RE001", + "file": ".github/workflows/cflite_batch.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "dogfood-gate.yml" + "rule_module": "research_extensions", + "type": "RE001", + "file": ".github/workflows/cflite_pr.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "dogfood-proofs-ci.yml" + "rule_module": "research_extensions", + "type": "RE001", + "file": ".github/workflows/ghcr-publish.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "formal-verification.yml" + "rule_module": "research_extensions", + "type": "RE001", + "file": ".github/workflows/label-triage.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "generator-generic-ossf-slsa3-publish.yml" + "rule_module": "research_extensions", + "type": "RE004", + "file": ".github/workflows/s4-loop.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "ghcr-publish.yml" + "rule_module": "research_extensions", + "type": "RE004", + "file": ".github/workflows/container-ci.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "idris2-abi-ci.yml" + "rule_module": "research_extensions", + "type": "RE005", + "file": ".github/workflows/server-boot-gate.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "live-provers.yml" + "rule_module": "research_extensions", + "type": "RE005", + "file": ".github/workflows/live-provers.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "mvp-smoke.yml" + "rule_module": "workflow_hardening", + "type": "WH008", + "file": ".github/workflows/scorecard.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "pages.yml" + "rule_module": "workflow_hardening", + "type": "WH008", + "file": ".github/workflows/secret-scanner.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "s4-loop.yml" + "rule_module": "workflow_hardening", + "type": "WH008", + "file": ".github/workflows/hypatia-scan.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "server-boot-gate.yml" + "rule_module": "workflow_hardening", + "type": "WH008", + "file": ".github/workflows/mirror.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "verification-proofs-cron.yml" + "rule_module": "structural_drift", + "type": "SD022", + "file": "docs/STALE-REFERENCE-TOMBSTONES.adoc", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "tombstone document: references to removed paths are intentional" }, { "severity": "medium", - "rule_module": "workflow_audit", - "type": "unpinned_action", - "file": "workflow-linter.yml" + "rule_module": "content_patterns", + "type": "download_then_run_shell", + "file": "echidna-playground/.github/workflows/mirror.yml", + "tracking_issue": "hyperpolymath/echidna#314", + "note": "pre-existing on main; grandfathered at re-arm, burn down under #314" } ] diff --git a/.machine_readable/bot_directives/echidnabot.a2ml b/.machine_readable/bot_directives/echidnabot.a2ml index eda6aa1a..fdb335fc 100644 --- a/.machine_readable/bot_directives/echidnabot.a2ml +++ b/.machine_readable/bot_directives/echidnabot.a2ml @@ -26,8 +26,9 @@ last-updated = "2026-04-25" mode = "regulator" [regulator] -# Threshold leaves a small flake budget. echidna's CI exercises 113 -# prover backends; transient ECHIDNA-binary unavailability or upstream +# Threshold leaves a small flake budget. echidna has 105 backend +# implementation files (141 ProverKind variants; docs/PROVER_COUNT.adoc is +# the single source for counts); transient ECHIDNA-binary unavailability or upstream # prover-binary install hiccups should not block the entire merge gate # when the rest of the matrix is solid. coverage-threshold = 90 # percent; merge releases at 90/100 provers passing diff --git a/.machine_readable/contractiles/dust/dust.k9.ncl b/.machine_readable/contractiles/dust/dust.k9.ncl index 0e06cbd5..be922a49 100644 --- a/.machine_readable/contractiles/dust/dust.k9.ncl +++ b/.machine_readable/contractiles/dust/dust.k9.ncl @@ -113,7 +113,7 @@ let base = import "../_base.ncl" in { kind = 'verisimdb, table = "contractile_executions", schema = "contractile_execution_v1", aux_tables = [ "dust_recovery_history" ] }, - { kind = 'drift_log, path = ".machine_readable/6a2/DRIFT.a2ml", + { kind = 'drift_log, path = ".machine_readable/descriptiles/DRIFT.a2ml", append_only = true }, ], @@ -167,7 +167,7 @@ let base = import "../_base.ncl" in signature_required = true, }, ], - signed_record_destination = ".machine_readable/6a2/ratification-.a2ml", + signed_record_destination = ".machine_readable/descriptiles/ratification-.a2ml", must_precede_work = true, }, diff --git a/.machine_readable/contractiles/must/must.k9.ncl b/.machine_readable/contractiles/must/must.k9.ncl index 2a7224ac..05d9e06e 100644 --- a/.machine_readable/contractiles/must/must.k9.ncl +++ b/.machine_readable/contractiles/must/must.k9.ncl @@ -135,7 +135,7 @@ let base = import "../_base.ncl" in }, { kind = 'drift_log, - path = ".machine_readable/6a2/DRIFT.a2ml", + path = ".machine_readable/descriptiles/DRIFT.a2ml", append_only = true, }, ], @@ -210,7 +210,7 @@ let base = import "../_base.ncl" in signature_required = true, }, ], - signed_record_destination = ".machine_readable/6a2/ratification-.a2ml", + signed_record_destination = ".machine_readable/descriptiles/ratification-.a2ml", must_precede_work = true, }, diff --git a/.machine_readable/contractiles/trust/trust.k9.ncl b/.machine_readable/contractiles/trust/trust.k9.ncl index fd0f5eb3..c253021a 100644 --- a/.machine_readable/contractiles/trust/trust.k9.ncl +++ b/.machine_readable/contractiles/trust/trust.k9.ncl @@ -140,7 +140,7 @@ let base = import "../_base.ncl" in }, { kind = 'drift_log, - path = ".machine_readable/6a2/DRIFT.a2ml", + path = ".machine_readable/descriptiles/DRIFT.a2ml", append_only = true, }, ], @@ -232,7 +232,7 @@ let base = import "../_base.ncl" in signature_required = true, }, ], - signed_record_destination = ".machine_readable/6a2/ratification-.a2ml", + signed_record_destination = ".machine_readable/descriptiles/ratification-.a2ml", must_precede_work = true, }, diff --git a/.machine_readable/descriptiles/META.a2ml b/.machine_readable/descriptiles/META.a2ml index 847de8f5..4485e195 100644 --- a/.machine_readable/descriptiles/META.a2ml +++ b/.machine_readable/descriptiles/META.a2ml @@ -8,14 +8,14 @@ full-name = "Extensible Cognitive Hybrid Intelligence for Deductive Neural Assis author = "Jonathan D.A. Jewell " license = "MPL-2.0" standard = "RSR 2026" -version = "2.2.0" -last-updated = "2026-04-28" +version = "2.3.0" +last-updated = "2026-10-05" status = "active" [project-context] name = "echidna" -completion-percentage = 94 -phase = "v2.2.0 — N-dim corpus + design-search + swarm landed" +completion-percentage = 100 # mirrors STATE.a2ml (the authority for status); v2.3.0 release scope only +phase = "v2.3.0 released — see STATE.a2ml for the current phase" notes = """ 2026-04-28: corpus subsystem expanded into an N-dimensional / 8- modality / cross-prover index, with simulated-annealing design-search @@ -25,7 +25,7 @@ docs/decisions/2026-04-28-corpus-and-design-search.adoc. [dependencies] primary = ["Rust", "Julia", "AffineScript", "Idris2", "Zig"] -secondary = ["Chapel", "Deno", "Guix", "Guix"] +secondary = ["Chapel", "Bun", "Guix"] [interfaces] graphql = 8081 diff --git a/.trusted-base-ignore b/.trusted-base-ignore index c343d2e9..44488b72 100644 --- a/.trusted-base-ignore +++ b/.trusted-base-ignore @@ -23,7 +23,7 @@ # These files are the *implementation* of the trust-pipeline's # axiom-tracker — they're proof infrastructure, not proof escapes. src/rust/verification/axiom_tracker.rs -crates/echidna-core-spark/src/axiom_tracker.rs +crates/echidna-core-creusot/src/axiom_tracker.rs # ───────────────────────────────────────────────────────────────────────────── # Hazard-classification helpers in the corpus extractor (NOT uses) diff --git a/AUTHORS.adoc b/AUTHORS.adoc index 46ba78ff..6ab26c8e 100644 --- a/AUTHORS.adoc +++ b/AUTHORS.adoc @@ -73,7 +73,7 @@ for the deliberation. === Contact * *GitHub Issues*: https://github.com/hyperpolymath/echidna/issues -* *Security*: see link:SECURITY.md[`+SECURITY.md+`] — use GitHub +* *Security*: see link:SECURITY.adoc[`+SECURITY.adoc+`] — use GitHub Security Advisories for vulnerabilities, not public issues. ''''' diff --git a/CLAUDE.md b/CLAUDE.md index a4e9adcb..96d270c5 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -87,7 +87,7 @@ Follow conventional commit format: - **Idris2**: Formal ABI specifications + totality proofs (`src/abi/`); zero `believe_me`, zero postulates, zero admits, enforced by `idris2-abi-ci.yml` - **Zig**: C-ABI FFI bridge (`ffi/zig/`, `src/zig_ffi/`) - **Chapel**: Optional parallel proof dispatch (`--features chapel`) -- **AffineScript + Deno**: the UI. ReScript was removed 2026-08 (banned language); the AffineScript-TEA compile pipeline is not wired yet — `just build-ui` fails deliberately rather than pretending (issues #117, #266) +- **AffineScript + Bun**: the UI (`just serve-ui` uses Bun; Deno is retired). ReScript was removed 2026-08 (banned language); the AffineScript-TEA compile pipeline is not wired yet — `just build-ui` fails deliberately rather than pretending (issues #117, #266) ### Prover Support @@ -134,7 +134,7 @@ Shape, by area: - **Chapel parallel layer (`--features chapel`)**: `ChapelParallelSearch` invoked by `dispatch.rs::verify_proof_parallel`; per-prover cwd/filename hooks in `tryProver`; L2.3 cancel-token preemption shipped; `parallelProofSearchSpeculative` (first-success-wins atomic-CAS) alongside best-of `parallelProofSearch`; `proofs/agda/ParallelSoundness.agda` formalises soundness, completeness, and cancellation-safety with zero postulate / admit / believe_me. L2.4+ (mutation parallelism, multi-locale, numeric hot paths, bench) gated on L1 Cap'n Proto and (for L2.5) a cluster runtime — see [`docs/handover/TODO.adoc`](docs/handover/TODO.adoc). - **Wave-3 container infrastructure**: per-prover images in `.containerization/Containerfile.wave3`; weekly cron in `container-ci.yml` runs stub-sentinel detection across all 8 Tier-3 cells. - **Julia ML layer**: logistic-regression tactic prediction shipped; Flux.jl scaffolds for GNN/Transformer training present but not yet trained on real data — corpus ready under `training_data/`. -- **Migrations in flight**: AffineScript → AffineScript-TEA (UI); npm → Deno (`echidna-playground`); CI workflow consolidation under the governance ruleset. +- **Migrations in flight**: AffineScript → AffineScript-TEA (UI); npm → Bun (`echidna-playground`); CI workflow consolidation under the governance ruleset. ## Useful Commands diff --git a/Cargo.lock b/Cargo.lock index bf610b18..81af6998 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -297,13 +297,13 @@ dependencies = [ [[package]] name = "async-trait" -version = "0.1.89" +version = "0.1.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9035ad2d096bed7955a320ee7e2230574d28fd3c3a0f186cbea1ff3c7eed5dbb" +checksum = "82f6aeea286b8eb4dd3431a1be1b59d290ace00f5bfd8e2a159bc2a05e2c1667" dependencies = [ "proc-macro2", "quote", - "syn 2.0.117", + "syn 3.0.3", ] [[package]] @@ -487,15 +487,6 @@ dependencies = [ "serde", ] -[[package]] -name = "capnp" -version = "0.26.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "58ddce707ad9fb2ae92770523cd0e17a0cf34e79b66a9ca4db2dd993535fe718" -dependencies = [ - "embedded-io", -] - [[package]] name = "capnp" version = "0.27.1" @@ -507,11 +498,11 @@ dependencies = [ [[package]] name = "capnpc" -version = "0.26.0" +version = "0.27.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "13aea06b902f885cb0313b11e900e96cd57fef775e9e601a96e14e1d655f3cd3" +checksum = "82ca16312ddb64529d31c8dc46148671c22e57b80134fa5f17811ad5a6a79492" dependencies = [ - "capnp 0.26.2", + "capnp", ] [[package]] @@ -1097,6 +1088,7 @@ dependencies = [ "rustyline", "serde", "serde_json", + "serde_json_canonicalizer", "sha2 0.11.0", "strum 0.28.0", "tempfile", @@ -1123,7 +1115,7 @@ dependencies = [ ] [[package]] -name = "echidna-core-spark" +name = "echidna-core-creusot" version = "0.1.0" dependencies = [ "serde", @@ -1202,7 +1194,7 @@ dependencies = [ "tower-http 0.7.0", "tracing", "tracing-subscriber", - "utoipa 6.0.0", + "utoipa", "utoipa-swagger-ui", "uuid", ] @@ -1211,7 +1203,7 @@ dependencies = [ name = "echidna-wire" version = "0.1.0" dependencies = [ - "capnp 0.27.1", + "capnp", "capnpc", ] @@ -3079,9 +3071,9 @@ dependencies = [ [[package]] name = "rustls" -version = "0.23.40" +version = "0.23.45" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef86cd5876211988985292b91c96a8f2d298df24e75989a43a3c73f2d4d8168b" +checksum = "0d41d731c7d2f962d1ccc364cec258de3c0e93b38c2fb3ba97ac74513048d634" dependencies = [ "log", "once_cell", @@ -3104,9 +3096,9 @@ dependencies = [ [[package]] name = "rustls-webpki" -version = "0.103.13" +version = "0.103.15" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61c429a8649f110dddef65e2a5ad240f747e85f7758a6bccc7e5777bd33f756e" +checksum = "f3c3cf1d8b1e7d4927e2d154c3fcb02979afb9939629c62cd9048d4f07b60ac2" dependencies = [ "ring", "rustls-pki-types", @@ -3158,6 +3150,12 @@ version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f" +[[package]] +name = "ryu-js" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "04d056b875a9d2e6cb9a61d127afee9ac5999b9f87bcb32079d1318e505be714" + [[package]] name = "safe_arch" version = "1.0.0" @@ -3300,6 +3298,17 @@ dependencies = [ "zmij", ] +[[package]] +name = "serde_json_canonicalizer" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fe52319a927259afbfa5180c5157cd8167edfd3e8c254f9558c7fef44c5649f2" +dependencies = [ + "ryu-js", + "serde", + "serde_json", +] + [[package]] name = "serde_path_to_error" version = "0.1.20" @@ -4149,18 +4158,6 @@ version = "0.2.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" -[[package]] -name = "utoipa" -version = "5.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8bde15df68e80b16c7d16b9616e80770ad158988daa56a27dccd1e55558b0160" -dependencies = [ - "indexmap", - "serde", - "serde_json", - "utoipa-gen 5.5.0", -] - [[package]] name = "utoipa" version = "6.0.0" @@ -4170,18 +4167,7 @@ dependencies = [ "indexmap", "serde", "serde_json", - "utoipa-gen 6.0.1", -] - -[[package]] -name = "utoipa-gen" -version = "5.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6ba0b99ee52df3028635d93840c797102da61f8a7bb3cf751032455895b52ef8" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.117", + "utoipa-gen", ] [[package]] @@ -4209,7 +4195,7 @@ dependencies = [ "serde", "serde_json", "url", - "utoipa 6.0.0", + "utoipa", "zip", ] diff --git a/Cargo.toml b/Cargo.toml index 2e84051d..36417740 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -60,8 +60,11 @@ rustyline = "18" blake3 = "1" tiny-keccak = { version = "2", features = ["shake"] } -# UUID -uuid = { version = "1.25.0", features = ["v4", "serde"] } +# UUID — minted only through src/rust/ids.rs: v7 record ids, v8 content ids. +uuid = { version = "1.25.0", features = ["v7", "v8", "serde"] } +# JCS (RFC 8785) canonical JSON, for ids::content_id. The estate's own +# ijson-jcs crate is not public, so this public build cannot depend on it. +serde_json_canonicalizer = "0.3" # Lazy statics lazy_static = "1" @@ -144,7 +147,7 @@ harness = false [workspace] members = [ "crates/echidna-core", - "crates/echidna-core-spark", + "crates/echidna-core-creusot", "crates/echidna-mcp", "crates/echidna-wire", "crates/typed_wasm", @@ -153,6 +156,5 @@ members = [ "src/interfaces/rest", ] exclude = [ - "echidnabot", "fuzz", ] diff --git a/Containerfile b/Containerfile index 10e7ad6c..ea6e3742 100644 --- a/Containerfile +++ b/Containerfile @@ -13,7 +13,7 @@ # ============================================================================= # Stage 1: Rust Builder # ============================================================================= -FROM cgr.dev/chainguard/wolfi-base:latest AS rust-builder +FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 AS rust-builder RUN apk add --no-cache \ rust \ @@ -45,7 +45,7 @@ RUN cargo build --release --bin echidna # ============================================================================= # Stage 2: Prover Installer (Z3 from official release, Lean via elan) # ============================================================================= -FROM cgr.dev/chainguard/wolfi-base:latest AS prover-installer +FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 AS prover-installer RUN apk add --no-cache \ curl \ @@ -74,7 +74,7 @@ RUN curl -fsSL https://raw.githubusercontent.com/leanprover/elan/master/elan-ini # ============================================================================= # Stage 3: Runtime Image (chainguard) # ============================================================================= -FROM cgr.dev/chainguard/wolfi-base:latest +FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 LABEL maintainer="Jonathan D.A. Jewell " LABEL org.opencontainers.image.source="https://github.com/hyperpolymath/echidna" diff --git a/HOL-o-extension/.machine_readable/6a2/ECOSYSTEM.a2ml b/HOL-o-extension/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 100% rename from HOL-o-extension/.machine_readable/6a2/ECOSYSTEM.a2ml rename to HOL-o-extension/.machine_readable/descriptiles/ECOSYSTEM.a2ml diff --git a/HOL-o-extension/.machine_readable/6a2/META.a2ml b/HOL-o-extension/.machine_readable/descriptiles/META.a2ml similarity index 100% rename from HOL-o-extension/.machine_readable/6a2/META.a2ml rename to HOL-o-extension/.machine_readable/descriptiles/META.a2ml diff --git a/HOL-o-extension/.machine_readable/6a2/STATE.a2ml b/HOL-o-extension/.machine_readable/descriptiles/STATE.a2ml similarity index 100% rename from HOL-o-extension/.machine_readable/6a2/STATE.a2ml rename to HOL-o-extension/.machine_readable/descriptiles/STATE.a2ml diff --git a/Justfile b/Justfile index 7fc65461..87629b02 100644 --- a/Justfile +++ b/Justfile @@ -532,9 +532,10 @@ build-ui: @echo "Sources: src/ui/tea/echidna_gui.affine; shell: src/ui/public/." @exit 1 -# Serve the static UI shell (no compile step) +# Serve the static UI shell (no compile step) on http://localhost:3000. +# Bun is the estate JavaScript runtime; Deno is retired (2026-09-22 ruling). serve-ui: - cd src/ui/public && deno run --allow-net --allow-read jsr:@std/http/file-server + cd src/ui/public && bun ../../../scripts/serve-static.js 3000 # Launch full ECHIDNA GUI (Backend + UI + Browser) gui: @@ -545,7 +546,7 @@ gui: cargo run -- server --port 8081 --cors > /dev/null 2>&1 & BACKEND_PID=$! echo "Started backend (PID $BACKEND_PID)" # Start UI server - (cd src/ui/public && deno run --allow-net --allow-read jsr:@std/http/file-server) > /dev/null 2>&1 & UI_PID=$! + (cd src/ui/public && bun ../../../scripts/serve-static.js 3000) > /dev/null 2>&1 & UI_PID=$! echo "Started UI server (PID $UI_PID)" # Cleanup on exit trap "kill $BACKEND_PID $UI_PID 2>/dev/null || true" EXIT @@ -783,15 +784,15 @@ verify-spark-crosscheck: build-spark # Run Creusot formal verification on the trust-pipeline kernel. # -# Prerequisites: Creusot + Why3 + Z3/CVC5 (see crates/echidna-core-spark/CREUSOT-SETUP.adoc). -# The nightly pin lives in crates/echidna-core-spark/rust-toolchain.toml. +# Prerequisites: Creusot + Why3 + Z3/CVC5 (see crates/echidna-core-creusot/CREUSOT-SETUP.adoc). +# The nightly pin lives in crates/echidna-core-creusot/rust-toolchain.toml. # # This recipe is currently in report-only mode: CI runs it and posts # results but does not block the merge until Stage 8c-M3. verify-trust-pipeline: - @echo "Running Creusot formal verification on echidna-core-spark..." + @echo "Running Creusot formal verification on echidna-core-creusot..." cargo +nightly creusot \ - -p echidna-core-spark \ + -p echidna-core-creusot \ -- \ --features creusot \ --why3 "$(which why3)" @@ -800,8 +801,8 @@ verify-trust-pipeline: # Stable-Rust test suite for the Creusot-annotated trust pipeline. # Runs on any Rust version; does not require Creusot or Why3. test-trust-pipeline: - cargo test -p echidna-core-spark - @echo "Trust-pipeline invariant tests passed ($(cargo test -p echidna-core-spark 2>&1 | grep 'test result' | head -1 | grep -oP '\d+ passed') tests)." + cargo test -p echidna-core-creusot + @echo "Trust-pipeline invariant tests passed ($(cargo test -p echidna-core-creusot 2>&1 | grep 'test result' | head -1 | grep -oP '\d+ passed') tests)." # ── Other ─────────────────────────────────────────────────── @@ -863,7 +864,7 @@ doctor: check_optional "Idris2" "idris2" check_optional "Zig" "zig" check_optional "Julia" "julia" - check_optional "Deno" "deno" + check_optional "Bun" "bun" check_optional "Chapel" "chpl" check_optional "panic-attack" "panic-attack" echo "" diff --git a/MAINTAINERS.adoc b/MAINTAINERS.adoc index 26b1b702..2b26045c 100644 --- a/MAINTAINERS.adoc +++ b/MAINTAINERS.adoc @@ -47,7 +47,7 @@ May be invited to become maintainers at the discretion of existing maintainers. For questions about project governance, open an issue or contact the maintainers listed above. For security disclosures, use the GitHub Security Advisories route documented in -link:SECURITY.md[`SECURITY.md`] — do NOT open public issues for +link:SECURITY.adoc[`SECURITY.adoc`] — do NOT open public issues for vulnerabilities. For high-level direction the canonical surfaces are: diff --git a/NOTICE b/NOTICE index 578bf411..fdfe9b9f 100644 --- a/NOTICE +++ b/NOTICE @@ -144,7 +144,7 @@ By contributing, you certify that: SECURITY -See SECURITY.md and .well-known/security.txt. +See SECURITY.adoc and .well-known/security.txt. Do not disclose security issues publicly until they have been addressed. ================================================================================ diff --git a/Project.toml b/Project.toml index a70895f8..421d7422 100644 --- a/Project.toml +++ b/Project.toml @@ -2,7 +2,7 @@ # SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors name = "ECHIDNA" -uuid = "00000000-0000-0000-0000-000000000000" # Generate proper UUID +uuid = "c2e75152-b2c9-4188-ae72-40d8a7dc1cd0" # UUIDv4: Julia package UUIDs are random v4 by ecosystem convention (Pkg.generate); exempt from the estate v7 standard as an externally-defined format authors = ["ECHIDNA Project Contributors"] version = "0.1.0" diff --git a/README.adoc b/README.adoc index 1be35d43..a2dd3456 100644 --- a/README.adoc +++ b/README.adoc @@ -550,7 +550,7 @@ governance ruleset. * link:CONTRIBUTING.md[Contributing Guidelines] * link:CODE_OF_CONDUCT.adoc[Code of Conduct] -* link:SECURITY.md[Security Policy] +* link:SECURITY.adoc[Security Policy] * link:CHANGELOG.adoc[Changelog] * link:docs/ROADMAP.adoc[Roadmap] * link:RSR_COMPLIANCE.adoc[RSR / CCCP Compliance Statement] diff --git a/RSR_COMPLIANCE.adoc b/RSR_COMPLIANCE.adoc index 1abc945c..fd31cf72 100644 --- a/RSR_COMPLIANCE.adoc +++ b/RSR_COMPLIANCE.adoc @@ -58,7 +58,7 @@ ECHIDNA diverges from the strict RSR template in three places: 3. *Extracted Rust crates*: workspace-member crates live in `crates/` alongside `src/rust/`. The split between `src/rust/` (binary + main library) and `crates/` (extracted workspace members like `echidna-mcp`, - `echidna-wire`, `echidna-core-spark`, `typed_wasm`) is intentional and + `echidna-wire`, `echidna-core-creusot`, `typed_wasm`) is intentional and documented in `Cargo.toml`. == Verifying compliance locally diff --git a/SECURITY.adoc b/SECURITY.adoc index e68a1279..3240cf7d 100644 --- a/SECURITY.adoc +++ b/SECURITY.adoc @@ -250,7 +250,7 @@ responsibly disclosing vulnerabilities: ''''' -*Document lineage*: revisions tracked via `+git log SECURITY.md+`; +*Document lineage*: revisions tracked via `+git log SECURITY.adoc+`; versioned alongside the project (see link:CHANGELOG.adoc[`+CHANGELOG.adoc+`]). This file is intentionally count-free and version-free in prose to avoid R5b drift against diff --git a/container/Containerfile b/container/Containerfile index 16aa930a..13d75960 100644 --- a/container/Containerfile +++ b/container/Containerfile @@ -12,7 +12,7 @@ # ============================================================================= # Stage 1: Builder # ============================================================================= -FROM cgr.dev/chainguard/wolfi-base:latest AS builder +FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 AS builder RUN apk add --no-cache \ rust \ @@ -32,7 +32,7 @@ RUN cargo build --release --bin echidna # ============================================================================= # Stage 2: Runtime # ============================================================================= -FROM cgr.dev/chainguard/wolfi-base:latest +FROM cgr.dev/chainguard/wolfi-base:latest@sha256:9c2092b053779e14c82fb50f77b37bcc38b7d2c83972352d5813280f9d035b03 LABEL org.opencontainers.image.title="ECHIDNA" \ org.opencontainers.image.description="Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance" \ diff --git a/crates/echidna-core-spark/CREUSOT-SETUP.adoc b/crates/echidna-core-creusot/CREUSOT-SETUP.adoc similarity index 95% rename from crates/echidna-core-spark/CREUSOT-SETUP.adoc rename to crates/echidna-core-creusot/CREUSOT-SETUP.adoc index 1f0a5c2e..fe1fda25 100644 --- a/crates/echidna-core-spark/CREUSOT-SETUP.adoc +++ b/crates/echidna-core-creusot/CREUSOT-SETUP.adoc @@ -1,6 +1,6 @@ == Creusot Setup Guide -How to run formal verification on `+echidna-core-spark+` using Creusot. +How to run formal verification on `+echidna-core-creusot+` using Creusot. === Prerequisites @@ -18,7 +18,7 @@ nightly and add it: [source,bash] ---- rustup toolchain install nightly-2024-05-01 # example — check current pin -rustup override set nightly-2024-05-01 --path crates/echidna-core-spark +rustup override set nightly-2024-05-01 --path crates/echidna-core-creusot ---- `+rust-toolchain.toml+` is at the crate root (added Stage 8c-M1) and @@ -66,7 +66,7 @@ From the repository root: [source,bash] ---- cargo +nightly creusot \ - -p echidna-core-spark \ + -p echidna-core-creusot \ -- \ --features creusot \ --why3 $(which why3) @@ -97,7 +97,7 @@ All obligations in `+impl_invariants+` are designed to discharge quickly `+.github/workflows/formal-verification.yml+` runs two jobs, both merge gates: -* `+stable-tests+`: `+cargo test -p echidna-core-spark+` on stable Rust +* `+stable-tests+`: `+cargo test -p echidna-core-creusot+` on stable Rust (~10 s). * `+creusot-verify+`: `+cargo +nightly creusot+` with Why3 + Z3 discharge. Requires `+apt-get install why3 z3 alt-ergo+` in the runner diff --git a/crates/echidna-core-spark/Cargo.toml b/crates/echidna-core-creusot/Cargo.toml similarity index 77% rename from crates/echidna-core-spark/Cargo.toml rename to crates/echidna-core-creusot/Cargo.toml index f3d25560..cdd05a74 100644 --- a/crates/echidna-core-spark/Cargo.toml +++ b/crates/echidna-core-creusot/Cargo.toml @@ -1,10 +1,10 @@ # SPDX-License-Identifier: MPL-2.0 [package] -name = "echidna-core-spark" +name = "echidna-core-creusot" version = "0.1.0" edition = "2021" -description = "Creusot-annotated trust pipeline kernel for ECHIDNA" +description = "Creusot-annotated (not yet proved) trust pipeline kernel for ECHIDNA" # crates.io requires an OSI-approved identifier; MPL-2.0 is the automatic # legal fallback for MPL-2.0 until PMPL achieves formal recognition. license = "MPL-2.0" @@ -19,6 +19,6 @@ serde = { version = "1", features = ["derive"] } [features] # Gate all Creusot-specific annotations behind this feature so that -# `cargo build -p echidna-core-spark` succeeds on stable Rust without +# `cargo build -p echidna-core-creusot` succeeds on stable Rust without # any Creusot installation. creusot = [] diff --git a/crates/echidna-core-spark/rust-toolchain.toml b/crates/echidna-core-creusot/rust-toolchain.toml similarity index 100% rename from crates/echidna-core-spark/rust-toolchain.toml rename to crates/echidna-core-creusot/rust-toolchain.toml diff --git a/crates/echidna-core-spark/src/axiom_tracker.rs b/crates/echidna-core-creusot/src/axiom_tracker.rs similarity index 100% rename from crates/echidna-core-spark/src/axiom_tracker.rs rename to crates/echidna-core-creusot/src/axiom_tracker.rs diff --git a/crates/echidna-core-spark/src/lib.rs b/crates/echidna-core-creusot/src/lib.rs similarity index 96% rename from crates/echidna-core-spark/src/lib.rs rename to crates/echidna-core-creusot/src/lib.rs index 7be66bfa..7c12b464 100644 --- a/crates/echidna-core-spark/src/lib.rs +++ b/crates/echidna-core-creusot/src/lib.rs @@ -1,6 +1,6 @@ // SPDX-License-Identifier: MPL-2.0 -//! # echidna-core-spark +//! # echidna-core-creusot //! //! Creusot-annotated trust-pipeline kernel for ECHIDNA. //! @@ -28,17 +28,25 @@ //! Build without it for normal stable-Rust use: //! //! ```text -//! cargo build -p echidna-core-spark # stable, no annotations -//! cargo +nightly creusot -p echidna-core-spark -- --features creusot +//! cargo build -p echidna-core-creusot # stable, no annotations +//! cargo +nightly creusot -p echidna-core-creusot -- --features creusot //! ``` //! -//! See [`CREUSOT-SETUP.md`](../CREUSOT-SETUP.md) for full toolchain setup. +//! See [`CREUSOT-SETUP.adoc`](../CREUSOT-SETUP.adoc) for full toolchain setup. //! -//! ## SPARK adoption stage +//! ## Verification status (honest) //! -//! This scaffold satisfies **Stage 8c** of the ECHIDNA ROADMAP: -//! "SPARK-verified trust kernel scaffold". The migration roadmap in -//! `.machine_readable/6a2/STATE.a2ml` tracks `axiom_tracker.rs` and +//! The annotations are **stated, not proved**. `creusot-contracts` is not yet +//! a dependency, the nightly pin predates current Creusot, and no CI run has +//! discharged a single obligation. What CI does run is the stable-Rust +//! `#[test]` mirror of every obligation. The crate was formerly named +//! `echidna-core-spark`; it is Creusot (Rust), not SPARK (Ada). +//! +//! ## Roadmap stage +//! +//! This scaffold is the **Stage 8c** artefact of the ECHIDNA ROADMAP +//! ("verified trust kernel scaffold"). The migration roadmap in +//! `.machine_readable/descriptiles/STATE.a2ml` tracks `axiom_tracker.rs` and //! `confidence.rs` as highest-leverage targets. //! //! ## Modules diff --git a/crates/echidna-core-spark/src/pareto.rs b/crates/echidna-core-creusot/src/pareto.rs similarity index 99% rename from crates/echidna-core-spark/src/pareto.rs rename to crates/echidna-core-creusot/src/pareto.rs index 01ec41f0..3ee979b7 100644 --- a/crates/echidna-core-spark/src/pareto.rs +++ b/crates/echidna-core-creusot/src/pareto.rs @@ -39,7 +39,7 @@ //! on stable Rust) and as `#[cfg_attr(feature = "creusot", …)]` //! attribute macros (activated during formal verification — currently //! commented out pending the toolchain pin in -//! `crates/echidna-core-spark/CREUSOT-SETUP.adoc`). +//! `crates/echidna-core-creusot/CREUSOT-SETUP.adoc`). use serde::{Deserialize, Serialize}; diff --git a/crates/echidna-core/src/types.rs b/crates/echidna-core/src/types.rs index e09158b5..f353fedf 100644 --- a/crates/echidna-core/src/types.rs +++ b/crates/echidna-core/src/types.rs @@ -42,7 +42,7 @@ use serde::{Deserialize, Serialize}; /// `with_*` methods, e.g.: /// /// ``` -/// use echidna::types::{TypeInfo, Multiplicity}; +/// use echidna_core::types::{TypeInfo, Multiplicity}; /// let info = TypeInfo::default().with_multiplicity(Multiplicity::Linear); /// assert_eq!(info.multiplicity, Some(Multiplicity::Linear)); /// ``` diff --git a/crates/echidna-mcp/src/main.rs b/crates/echidna-mcp/src/main.rs index d6bf3074..5fe92e17 100644 --- a/crates/echidna-mcp/src/main.rs +++ b/crates/echidna-mcp/src/main.rs @@ -21,7 +21,7 @@ use rmcp::{ handler::server::{router::tool::ToolRouter, wrapper::Parameters}, - model::{ServerCapabilities, ServerInfo}, + model::{ServerCapabilities, ServerConfig}, schemars::JsonSchema, tool, tool_handler, tool_router, transport::stdio, @@ -256,8 +256,8 @@ impl EchidnaMcp { #[tool_handler(router = self.tool_router)] impl ServerHandler for EchidnaMcp { - fn get_info(&self) -> ServerInfo { - let mut info = ServerInfo::default(); + fn get_info(&self) -> ServerConfig { + let mut info = ServerConfig::default(); info.capabilities = ServerCapabilities::builder().enable_tools().build(); info.instructions = Some( "ECHIDNA MCP server. Call `prove` with a proof-file path and \ diff --git a/crates/echidna-wire/Cargo.toml b/crates/echidna-wire/Cargo.toml index 59e6f62d..79490153 100644 --- a/crates/echidna-wire/Cargo.toml +++ b/crates/echidna-wire/Cargo.toml @@ -14,4 +14,4 @@ build = "build.rs" capnp = "0.27" [build-dependencies] -capnpc = "0.26" +capnpc = "0.27" diff --git a/deno.lock b/deno.lock deleted file mode 100644 index 77b75dbe..00000000 --- a/deno.lock +++ /dev/null @@ -1,11 +0,0 @@ -{ - "version": "5", - "specifiers": { - "jsr:@std/yaml@*": "1.1.2" - }, - "jsr": { - "@std/yaml@1.1.2": { - "integrity": "de612653c036749ba2044165e316f52412b0f0698afffb7ee80b5331d6d2abae" - } - } -} diff --git a/docs/CORPUS-ADAPTERS.adoc b/docs/CORPUS-ADAPTERS.adoc index 05bdaac7..d83f8c2b 100644 --- a/docs/CORPUS-ADAPTERS.adoc +++ b/docs/CORPUS-ADAPTERS.adoc @@ -32,7 +32,7 @@ sorry, oops, consts, nitpick, quickcheck |*NEW 2026-06-01* |*metamath* |`+*.mm+` |https://github.com/metamath/set.mm |`+$a+` axiom usage, `+?+` admitted in proof |*NEW 2026-06-01* -|*mizar* |`+*.miz+`, `+*.abs+` |http://mizar.org/version/8.1.14/mml/ +|*mizar* |`+*.miz+`, `+*.abs+` |https://mizar.org/version/current/mml/ |`+@proof+` sketch, commented-theorem, consider-without-proof |*NEW 2026-06-01* diff --git a/docs/DEBT.adoc b/docs/DEBT.adoc index 1ba1caa6..545a0841 100644 --- a/docs/DEBT.adoc +++ b/docs/DEBT.adoc @@ -315,11 +315,12 @@ destinations*: git grep -n '6a2/' -- '*.ncl' ---- -Those were left alone deliberately: `+6a2+` is a concept name there, not -a stale path, and changing a contractile’s evidence sink is a semantic -decision. But the directory does not exist, so any drift-log write has -nowhere to land. Confirm whether the sink should be created or -repointed. +*Resolved 2026-10-05 (firstrun/20261005):* the write destinations were +repointed to `+.machine_readable/descriptiles/+`, the directory that +exists. rsr-template-repo forbids any contractile writing to `+6a2/+`, +so repointing (not recreating) is the only conformant choice. The two +sub-project `+6a2/+` directories (`+echidna-playground/+`, +`+HOL-o-extension/+`) moved to `+descriptiles/+` in the same change. ''''' diff --git a/docs/MIZAR_QUICK_START.adoc b/docs/MIZAR_QUICK_START.adoc index 9dc98bd0..850e0312 100644 --- a/docs/MIZAR_QUICK_START.adoc +++ b/docs/MIZAR_QUICK_START.adoc @@ -9,7 +9,7 @@ + [source,bash] ---- -# Download from http://mizar.org +# Download from https://mizar.org # Or use package manager: sudo apt-get install mizar # Debian/Ubuntu ---- @@ -414,9 +414,9 @@ structure - Correct operator syntax (`+\/+` not `+∪+`) === Resources -* *Mizar Homepage*: http://mizar.org -* *MML Browser*: http://mizar.org/version/current/html/ -* *Mizar Tutorial*: http://mizar.org/project/bibliography.html +* *Mizar Homepage*: https://mizar.org +* *MML Browser*: https://mizar.org/version/current/html/ +* *Mizar Tutorial*: https://mizar.org/project/bibliography.html * *ECHIDNA Docs*: /home/user/echidna/docs/ * *Full Backend Docs*: /home/user/echidna/docs/MIZAR_BACKEND.md diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc index ceedba65..6ff24141 100644 --- a/docs/ROADMAP.adoc +++ b/docs/ROADMAP.adoc @@ -122,7 +122,7 @@ Stage 7 Sovereign tooling surround the rest of the ecosystem Stage 8 Self‑verified ECHIDNA proves ECHIDNA 8a Idris2 meta‑proofs extend from 32 modules to full kernel 8b Agda meta‑proofs extend from 12 modules - 8c SPARK‑verified trust kernel crates/echidna-core-spark/ + 8c Verified trust kernel spark/ (Ada/SPARK) + crates/echidna-core-creusot/ (Creusot, stated not proved) 8d panic‑attack hardened proptest + AFL++ nightly .... @@ -175,8 +175,9 @@ Model → Msg → Update loop, talks to core over Cap’n Proto WebSocket |"`LOL i18n`" |Not present |*`+locale/+`* with LOL‑sourced translations; `+t!()+` macro for every user‑facing string -|"`Rust/SPARK base stable`" |Rust only |*`+crates/echidna-core-spark/+`* -holds the Ada/SPARK‑verified kernel (axiom scanning, trust‑level +|"`Rust/SPARK base stable`" |Rust only |*`+spark/+`* +holds the Ada/SPARK‑verified kernel (with a Creusot‑annotated Rust mirror in +`+crates/echidna-core-creusot/+`) (axiom scanning, trust‑level computation); proved free of runtime errors; called from Rust via C ABI |"`16‑endpoint Zig ABI`" |4 shared libs, endpoint count unverified diff --git a/docs/STALE-REFERENCE-TOMBSTONES.adoc b/docs/STALE-REFERENCE-TOMBSTONES.adoc index 0441b0b3..ad96037f 100644 --- a/docs/STALE-REFERENCE-TOMBSTONES.adoc +++ b/docs/STALE-REFERENCE-TOMBSTONES.adoc @@ -90,7 +90,7 @@ this is the reason the sweep checks target existence rather than blindly rewriting every `.md` it sees. 47 references fall in this class across the 21 tracked `+.md+` files: `+SECURITY.md+`, `+CLAUDE.md+`, `+GEMINI.md+`, `+.github/CONTRIBUTING.md+`, `+.github/PROVEN-INTEGRATION.md+`, -`+docs/wiki/*.md+` and the GitLab issue/MR templates. In particular +`+docs/wikis/*.md+` and the GitLab issue/MR templates. In particular `+SECURITY.md+` coexists with `+SECURITY.adoc+` and is *not* stale; an earlier, looser version of this sweep rewrote link in `+AUTHORS.adoc+` (`+link:SECURITY.md+`) and was caught by this check. diff --git a/docs/SUPPORTED_PROVERS.adoc b/docs/SUPPORTED_PROVERS.adoc index 1138448c..262069cc 100644 --- a/docs/SUPPORTED_PROVERS.adoc +++ b/docs/SUPPORTED_PROVERS.adoc @@ -38,7 +38,7 @@ external binary — pure-Rust implementation in Light: https://github.com/jrh13/hol-light |Mizar |Tarski–Grothendieck set theory |`+mizf+`, `+verifier+` -|http://mizar.org/system/index.html +|https://mizar.org/system/index.html |PVS |Prototype Verification System |`+pvs+` |https://pvs.csl.sri.com/ diff --git a/docs/decisions/2026-10-05-id-minting.adoc b/docs/decisions/2026-10-05-id-minting.adoc new file mode 100644 index 00000000..66835f68 --- /dev/null +++ b/docs/decisions/2026-10-05-id-minting.adoc @@ -0,0 +1,43 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += ADR: one ID-minting module (UUIDv7 records, UUIDv8 content) +:revdate: 2026-10-05 +:status: accepted (owner decision, delegated 2026-10-05) + +== Context + +Before this change echidna minted random UUIDv4 values at 28 call sites +(`git grep -n 'Uuid::new_v4' -- '*.rs'` on `main` at `b761b3a`): proof ids in +the REST, gRPC and GraphQL interfaces, session ids, dispatch attempt ids, and +temp-file names in the prover backends. Estate canon +(`standards/docs/UUID-V7-ESTATE-STANDARD.adoc`) requires UUIDv7 from a library +API, and the owner additionally asked for deterministic content ids. + +== Decision + +All minting goes through `src/rust/ids.rs` (`echidna::ids`): + +* `new_record_id()` -> UUIDv7 for events and records (proof requests, + sessions, attempts, runs, findings). Monotonic within a process. +* `content_id(value)` -> UUIDv8 per RFC 9562 Appendix B.2: SHA-256 over the + JCS (RFC 8785) canonical bytes of `value`, first 16 bytes, version nibble + `8`, variant bits `10`. For proof goals, prove results, corpus entries and + octads. +* `temp_token()` -> a hyphen-free v7, for temp-file names only. + +JCS comes from the public `serde_json_canonicalizer` crate. The estate crate +`hyperpolymath/ijson-jcs` is private on GitHub, so a public repository cannot +build against it. + +Julia package UUIDs (`Project.toml`) are outside this module: they are an +externally-defined format and stay random v4 by Julia convention. + +== Status of the parts (honest) + +* `new_record_id` / `temp_token`: implemented, tested, wired into every former + v4 site. +* `content_id`: implemented and tested (same JCS content -> same id; + version/variant bits; planted-control recomputation). **Not yet wired**: + corpus entries, octads and goals still use their existing identity hashes + (`proof_encoding.rs`); switching them changes stored identifiers and needs + its own migration. diff --git a/docs/wiki/Architecture.md b/docs/wikis/Architecture.md similarity index 100% rename from docs/wiki/Architecture.md rename to docs/wikis/Architecture.md diff --git a/docs/wiki/FAQ.md b/docs/wikis/FAQ.md similarity index 100% rename from docs/wiki/FAQ.md rename to docs/wikis/FAQ.md diff --git a/docs/wiki/Getting-Started.md b/docs/wikis/Getting-Started.md similarity index 100% rename from docs/wiki/Getting-Started.md rename to docs/wikis/Getting-Started.md diff --git a/docs/wiki/Guides.md b/docs/wikis/Guides.md similarity index 100% rename from docs/wiki/Guides.md rename to docs/wikis/Guides.md diff --git a/docs/wiki/Home.md b/docs/wikis/Home.md similarity index 62% rename from docs/wiki/Home.md rename to docs/wikis/Home.md index fb853e4d..8ac9331e 100644 --- a/docs/wiki/Home.md +++ b/docs/wikis/Home.md @@ -20,7 +20,7 @@ When the wiki and the repo disagree, **the repo wins**: -- [`README.md`](https://github.com/hyperpolymath/echidna/blob/main/README.md) — primary project README +- [`README.adoc`](https://github.com/hyperpolymath/echidna/blob/main/README.adoc) — primary project README - [`CLAUDE.md`](https://github.com/hyperpolymath/echidna/blob/main/CLAUDE.md) — codebase orientation - [`docs/ARCHITECTURE.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/ARCHITECTURE.adoc) — current architecture - [`docs/PROVER_COUNT.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.adoc) — tier table @@ -30,6 +30,36 @@ When the wiki and the repo disagree, **the repo wins**: - [`RSR_COMPLIANCE.adoc`](https://github.com/hyperpolymath/echidna/blob/main/RSR_COMPLIANCE.adoc) — RSR / CCCP compliance statement - [`.machine_readable/descriptiles/STATE.a2ml`](https://github.com/hyperpolymath/echidna/blob/main/.machine_readable/descriptiles/STATE.a2ml) — machine-readable state +## Capability status (honest, 2026-10-05) + +Each row says how far the capability actually goes. The words are used +strictly and none implies the next: **implemented** (code exists), +**wired** (reachable from the CLI/API), **tested** (exercised by an automated +test), **CI-gated** (a workflow runs it on every PR), **proved** (machine-checked +proof), **deployed** (running somewhere for users). Evidence: workflow runs on +`main` at `b761b3a` (paginated check-runs) plus the repository at the same +commit. + +| Capability | Status | Not yet | +|---|---|---| +| Rust core, CLI, REPL (`echidna prove/verify/search/…`) | implemented, wired, tested (`cargo test`) | Rust CI was in `startup_failure` on `main` from 2026-07 to 2026-10; restored by the 2026-10-05 start-point PR | +| 12 core backends (`GET /api/provers`) | implemented, wired, live-tested (T1/T2 live-prover matrices green) | — | +| Wider backend surface (see [`docs/PROVER_COUNT.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/PROVER_COUNT.adoc)) | implemented | Tier-4 backends are mock-only; the HP-ecosystem type-checker backends call `typell --discipline` / `tropical-type-check`, which upstream does not provide, so they are **not wired** | +| Trust pipeline (integrity, certificates, axioms, confidence, mutation, Pareto, statistics) | implemented, wired into `dispatch.rs`, unit-tested | not proved | +| Idris2 ABI (`src/abi/`) | type-checked, CI-gated (`idris2-abi-ci.yml`) | — | +| Dogfood proof corpus (`proofs/{coq,lean,agda}`) | CI-gated (`dogfood-proofs-ci.yml`) | — | +| Agda meta-checker | implemented | its workflow was in `startup_failure` on `main` | +| Creusot trust kernel (`crates/echidna-core-creusot`) | annotations **stated**; stable-Rust test mirror runs in CI | **not proved**: no obligation has been discharged; the Creusot job is manual-only | +| Ada/SPARK kernel (`spark/`) | implemented; `spark-theatre-gate` green | proof status not re-verified in this pass | +| Chapel parallel search (`--features chapel`) | implemented, builds in CI | the "real Chapel library" job is allow-fail and red | +| Julia ML (tactic prediction, GNN) | logistic-regression predictor implemented | GNN training runs offline; not CI-tested | +| REST / gRPC / GraphQL servers | implemented; server boot gate green | — | +| UI | static shell (`just serve-ui`, Bun) | AffineScript-TEA compile pipeline not wired (`just build-ui` fails on purpose) | +| ID minting (`echidna::ids`) | UUIDv7 record ids: implemented, wired, tested. UUIDv8 content ids (SHA-256 over JCS): implemented, tested | content ids not yet used for goals/corpus/octads | +| `echidna prove --output json` (`echidna.prove.result/1`) | — | not implemented yet | +| Containers | built in CI | publication not verified | +| Forge mirrors | GitLab, Codeberg, SourceHut, Radicle succeed | Bitbucket, Disroot, Gitea mirror jobs fail | + ## Core invariants 1. **ML suggests; provers verify.** Neural components rank, route, propose. Formal provers carry the trust. @@ -42,8 +72,8 @@ When the wiki and the repo disagree, **the repo wins**: - **4 arbitration mechanisms** — portfolio majority-vote, Bayesian posterior, Dempster-Shafer belief combination, Pareto multi-objective frontier. - **6 cross-prover exchange formats** — OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi. - **11-step trust pipeline** — integrity → portfolio → certificates → axioms → confidence → mutation → pareto → statistics → emission (see Architecture page). -- **Polyglot stack** — Rust core, Julia ML sidecar, Idris2/Agda formal proofs, Zig FFI, Chapel parallel, AffineScript/Deno UI (AffineScript removed 2026-08; the TEA compile pipeline is not wired yet — issues #117/#266). -- **Guix-only package management** — sealed-container escape hatch for the non-free tail. (Guix fallback was deprecated in the 2026-05-18 estate ruling and fully removed estate-wide on 2026-06-01.) +- **Polyglot stack** — Rust core, Julia ML sidecar, Idris2/Agda formal proofs, Zig FFI, Chapel parallel, AffineScript UI with a static shell served by Bun (ReScript removed 2026-08; Deno retired 2026-09; the AffineScript-TEA compile pipeline is not wired yet — issues #117/#266). +- **Guix-only package management** — sealed-container escape hatch for the non-free tail. (The Nix fallback was deprecated in the 2026-05-18 estate ruling and fully removed estate-wide on 2026-06-01.) - **Justfile, not Make. Podman, not Docker.** ## Recent major work @@ -53,6 +83,6 @@ The 2026-06-01 **prover/corpus/vocab/synonyms/arbitration saturation campaign** - [`docs/CORPUS-ADAPTERS.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/CORPUS-ADAPTERS.adoc) — 17-adapter index with per-adapter source URLs, hazard flags, and downstream wiring (`suggest` / `octad-emit` / GNN training). - [`docs/architecture/VERISIM-ER-SCHEMA.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/architecture/VERISIM-ER-SCHEMA.adoc) — VeriSim ↔ ECHIDNA E-R schema (12 entities + 7 relationships, each with Rust struct + VeriSimDB table + Cap'n Proto schema + PK/FK). - [`docs/decisions/2026-06-01-saturation-campaign.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/decisions/2026-06-01-saturation-campaign.adoc) — ADR documenting the ordered marginal-benefit hierarchy and the decision to execute levers (1)–(6) and defer (7) GNN-training. -- [`docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/handover/PROVER-CORPUS-SATURATION-LANE.md) — saturation lane handover with sibling-branch collision avoidance. +- [`docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc`](https://github.com/hyperpolymath/echidna/blob/main/docs/handover/PROVER-CORPUS-SATURATION-LANE.adoc) — saturation lane handover with sibling-branch collision avoidance. The **dogfood proof corpus is now CI-gated**: every theorem under `proofs/{coq,lean,agda}` and the `src/idris` validator type-checks on each PR (`dogfood-proofs-ci.yml` + `idris2-abi-ci.yml`), each driven by a `just proofs-*` recipe — closing a gap where the corpus had no CI. Run it locally via `just proofs`; see [Getting Started](Getting-Started). diff --git a/docs/wiki/README.md b/docs/wikis/README.md similarity index 96% rename from docs/wiki/README.md rename to docs/wikis/README.md index 76c1f061..6d6a5d4c 100644 --- a/docs/wiki/README.md +++ b/docs/wikis/README.md @@ -12,10 +12,10 @@ is `master`, not `main`. ```bash git clone https://github.com/hyperpolymath/echidna.wiki.git /tmp/echidna-wiki for f in Home Architecture Getting-Started FAQ Guides Troubleshooting; do - cp docs/wiki/"$f".md /tmp/echidna-wiki/"$f".md + cp docs/wikis/"$f".md /tmp/echidna-wiki/"$f".md done git -C /tmp/echidna-wiki add -A -git -C /tmp/echidna-wiki commit -m "docs: sync wiki from docs/wiki/" +git -C /tmp/echidna-wiki commit -m "docs: sync wiki from docs/wikis/" git -C /tmp/echidna-wiki push origin master ``` diff --git a/docs/wiki/Troubleshooting.md b/docs/wikis/Troubleshooting.md similarity index 100% rename from docs/wiki/Troubleshooting.md rename to docs/wikis/Troubleshooting.md diff --git a/echidna-playground/.github/workflows/codeql.yml b/echidna-playground/.github/workflows/codeql.yml index 799b55d9..6f7c22c7 100644 --- a/echidna-playground/.github/workflows/codeql.yml +++ b/echidna-playground/.github/workflows/codeql.yml @@ -46,7 +46,7 @@ jobs: uses: actions/checkout@11bd71901bbe5b1630ceea73d27597364c9af683 # v4.2.2 - name: Initialize CodeQL - uses: github/codeql-action/init@ea9e4e37992a54ee68a9571571f9a567d8f90f78 # v3.28.0 + uses: github/codeql-action/init@48ab28a6f5dbc2a99bf1e0131198dd8f1df78169 # v3.28.0 with: languages: ${{ matrix.language }} build-mode: ${{ matrix.build-mode }} @@ -63,6 +63,6 @@ jobs: echo "Configure your build command above for manual build mode languages" - name: Perform CodeQL Analysis - uses: github/codeql-action/analyze@ea9e4e37992a54ee68a9571571f9a567d8f90f78 # v3.28.0 + uses: github/codeql-action/analyze@48ab28a6f5dbc2a99bf1e0131198dd8f1df78169 # v3.28.0 with: category: "/language:${{ matrix.language }}" diff --git a/echidna-playground/.github/workflows/secret-scanner.yml b/echidna-playground/.github/workflows/secret-scanner.yml index 0899a46e..934af958 100644 --- a/echidna-playground/.github/workflows/secret-scanner.yml +++ b/echidna-playground/.github/workflows/secret-scanner.yml @@ -14,7 +14,7 @@ jobs: with: fetch-depth: 0 # Full history for scanning - name: TruffleHog Secret Scan - uses: trufflesecurity/trufflehog@8a8ef8526528d8a4ff3e2c90be08e25ef8efbd9b # v3 + uses: trufflesecurity/trufflehog@4dd8831c5f12599465d4d45c3c447b4018a34c85 # v3.97.9 with: extra_args: --only-verified --fail # Rust-specific: Check for hardcoded crypto values diff --git a/echidna-playground/.github/workflows/security-checks.yml b/echidna-playground/.github/workflows/security-checks.yml index 658f613c..92635558 100644 --- a/echidna-playground/.github/workflows/security-checks.yml +++ b/echidna-playground/.github/workflows/security-checks.yml @@ -20,7 +20,7 @@ jobs: with: fetch-depth: 0 - name: Detect secrets with TruffleHog - uses: trufflesecurity/trufflehog@8a8ef8526528d8a4ff3e2c90be08e25ef8efbd9b # v3 + uses: trufflesecurity/trufflehog@4dd8831c5f12599465d4d45c3c447b4018a34c85 # v3.97.9 with: extra_args: --only-verified --fail dependency-review: diff --git a/echidna-playground/.machine_readable/6a2/AGENTIC.a2ml b/echidna-playground/.machine_readable/descriptiles/AGENTIC.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/AGENTIC.a2ml rename to echidna-playground/.machine_readable/descriptiles/AGENTIC.a2ml diff --git a/echidna-playground/.machine_readable/6a2/ECOSYSTEM.a2ml b/echidna-playground/.machine_readable/descriptiles/ECOSYSTEM.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/ECOSYSTEM.a2ml rename to echidna-playground/.machine_readable/descriptiles/ECOSYSTEM.a2ml diff --git a/echidna-playground/.machine_readable/6a2/META.a2ml b/echidna-playground/.machine_readable/descriptiles/META.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/META.a2ml rename to echidna-playground/.machine_readable/descriptiles/META.a2ml diff --git a/echidna-playground/.machine_readable/6a2/NEUROSYM.a2ml b/echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/NEUROSYM.a2ml rename to echidna-playground/.machine_readable/descriptiles/NEUROSYM.a2ml diff --git a/echidna-playground/.machine_readable/6a2/PLAYBOOK.a2ml b/echidna-playground/.machine_readable/descriptiles/PLAYBOOK.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/PLAYBOOK.a2ml rename to echidna-playground/.machine_readable/descriptiles/PLAYBOOK.a2ml diff --git a/echidna-playground/.machine_readable/6a2/STATE.a2ml b/echidna-playground/.machine_readable/descriptiles/STATE.a2ml similarity index 100% rename from echidna-playground/.machine_readable/6a2/STATE.a2ml rename to echidna-playground/.machine_readable/descriptiles/STATE.a2ml diff --git a/echidna-playground/examples/web-project-deno.json b/echidna-playground/examples/web-project-deno.json deleted file mode 100644 index ee775a44..00000000 --- a/echidna-playground/examples/web-project-deno.json +++ /dev/null @@ -1,20 +0,0 @@ -{ - "// NOTE": "Example deno.json for AffineScript web projects", - "tasks": { - "build": "deno run -A npm:affinescript", - "clean": "deno run -A npm:affinescript clean", - "watch": "deno run -A npm:affinescript -w", - "serve": "deno run -A jsr:@std/http/file-server .", - "test": "deno test --allow-all" - }, - "imports": { - "affinescript": "^12.0.0", - "@affinescript/core": "npm:@affinescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/affinescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/affinescript/src/" - }, - "compilerOptions": { - "allowJs": true, - "checkJs": false - } -} diff --git a/examples/web-project-deno.json b/examples/web-project-deno.json deleted file mode 100644 index ee775a44..00000000 --- a/examples/web-project-deno.json +++ /dev/null @@ -1,20 +0,0 @@ -{ - "// NOTE": "Example deno.json for AffineScript web projects", - "tasks": { - "build": "deno run -A npm:affinescript", - "clean": "deno run -A npm:affinescript clean", - "watch": "deno run -A npm:affinescript -w", - "serve": "deno run -A jsr:@std/http/file-server .", - "test": "deno test --allow-all" - }, - "imports": { - "affinescript": "^12.0.0", - "@affinescript/core": "npm:@affinescript/core@^1.6.0", - "safe-dom/": "https://raw.githubusercontent.com/hyperpolymath/affinescript-dom-mounter/main/src/", - "proven/": "../proven/bindings/affinescript/src/" - }, - "compilerOptions": { - "allowJs": true, - "checkJs": false - } -} diff --git a/k9iser.toml b/k9iser.toml index 1d1b33b9..29b113a0 100644 --- a/k9iser.toml +++ b/k9iser.toml @@ -3,7 +3,7 @@ # # k9iser manifest for echidna # Generates K9 contracts from repo configuration files. -# echidna is a neurosymbolic theorem proving platform (Rust + Deno) +# echidna is a neurosymbolic theorem proving platform (Rust + Julia; Bun for the static UI shell) [project] name = "echidna" @@ -14,11 +14,6 @@ path = "Cargo.toml" type = "cargo" output = "generated/k9iser/cargo-manifest.k9" -[[source]] -path = "deno.json" -type = "deno" -output = "generated/k9iser/deno-workspace.k9" - [[source]] path = "Justfile" type = "justfile" @@ -55,6 +50,3 @@ severity = "warn" rule = "workflows includes hypatia-scan" severity = "error" -[[constraint]] -rule = "deno.imports has no npm: specifiers" -severity = "error" diff --git a/mise.lock b/mise.lock new file mode 100644 index 00000000..9867ca89 --- /dev/null +++ b/mise.lock @@ -0,0 +1,395 @@ +# @generated - this file is auto-generated by `mise lock` https://mise.jdx.dev/dev-tools/mise-lock.html + +[[tools.bun]] +version = "1.3.14" +backend = "core:bun" + +[tools.bun."platforms.linux-arm64"] +checksum = "sha256:a27ffb63a8310375836e0d6f668ae17fa8d8d18b88c37c821c65331973a19a3b" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-aarch64.zip" + +[tools.bun."platforms.linux-arm64-musl"] +checksum = "sha256:b98e0ad3625c5c00d1d5b5ff55605c7adddbfae151861e68ade57b2d3b8703bb" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-aarch64-musl.zip" + +[tools.bun."platforms.linux-x64"] +checksum = "sha256:951ee2aee855f08595aeec6225226a298d3fea83a3dcd6465c09cbccdf7e848f" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-x64.zip" + +[tools.bun."platforms.linux-x64-baseline"] +checksum = "sha256:a063908ae08b7852ca10939bbdc6ceed3ddabce8fb9402dce83d65d73b36e6c7" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-x64-baseline.zip" + +[tools.bun."platforms.linux-x64-musl"] +checksum = "sha256:14bd9aedeebf1dba67e8def9531c89bc989ecfdf1de42e5bfcaf1b8cd9294719" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-x64-musl.zip" + +[tools.bun."platforms.linux-x64-musl-baseline"] +checksum = "sha256:56a7d6806cf155536c0178f0ea5fbd098e684fa509ebdb4fc0a7e19fb65382dc" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-linux-x64-musl-baseline.zip" + +[tools.bun."platforms.macos-arm64"] +checksum = "sha256:d8b96221828ad6f97ac7ac0ab7e95872341af763001e8803e8267652c2652620" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-darwin-aarch64.zip" + +[tools.bun."platforms.macos-x64"] +checksum = "sha256:4183df3374623e5bab315c547cfa0974533cd457d86b73b639f7a87974cd6633" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-darwin-x64.zip" + +[tools.bun."platforms.macos-x64-baseline"] +checksum = "sha256:3e35ad6f53971a9834bf9e6786e2adf72b5f1921cc9a9c5fde073d2972944076" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-darwin-x64-baseline.zip" + +[tools.bun."platforms.windows-x64"] +checksum = "sha256:0a0620930b6675d7ba440e81f4e0e00d3cfbe096c4b140d3fff02205e9e18922" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-windows-x64.zip" + +[tools.bun."platforms.windows-x64-baseline"] +checksum = "sha256:538f9c846355d9e847b2671bc00c47da4229a0befb24df3282b739770f3b475f" +url = "https://github.com/oven-sh/bun/releases/download/bun-v1.3.14/bun-windows-x64-baseline.zip" + +[[tools.julia]] +version = "1.12.6" +backend = "http:julia" + +[tools.julia.options] +format = "zip" + +[tools.julia."platforms.linux-arm64"] +checksum = "sha256:029b93b857bd0ffd627f9a8580d3bbaa63daf008d7b7aed02fbceb8fd57c4899" +url = "https://julialang-s3.julialang.org/bin/linux/aarch64/1.12/julia-1.12.6-linux-aarch64.tar.gz" + +[tools.julia."platforms.linux-arm64-musl"] +checksum = "sha256:029b93b857bd0ffd627f9a8580d3bbaa63daf008d7b7aed02fbceb8fd57c4899" +url = "https://julialang-s3.julialang.org/bin/linux/aarch64/1.12/julia-1.12.6-linux-aarch64.tar.gz" + +[tools.julia."platforms.linux-x64"] +checksum = "sha256:bbabf3bef19421a9dbd24a767d807606ab85e444323b5a1c73ffe293fa3d079a" +url = "https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.6-linux-x86_64.tar.gz" + +[tools.julia."platforms.linux-x64-baseline"] +checksum = "sha256:bbabf3bef19421a9dbd24a767d807606ab85e444323b5a1c73ffe293fa3d079a" +url = "https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.6-linux-x86_64.tar.gz" + +[tools.julia."platforms.linux-x64-musl"] +checksum = "sha256:bbabf3bef19421a9dbd24a767d807606ab85e444323b5a1c73ffe293fa3d079a" +url = "https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.6-linux-x86_64.tar.gz" + +[tools.julia."platforms.linux-x64-musl-baseline"] +checksum = "sha256:bbabf3bef19421a9dbd24a767d807606ab85e444323b5a1c73ffe293fa3d079a" +url = "https://julialang-s3.julialang.org/bin/linux/x64/1.12/julia-1.12.6-linux-x86_64.tar.gz" + +[tools.julia."platforms.macos-arm64"] +checksum = "sha256:277d82fbd2eda99d0963b3e41f3dc979d7486f181399f8430fb637318ccd6a31" +url = "https://julialang-s3.julialang.org/bin/mac/aarch64/1.12/julia-1.12.6-macaarch64.tar.gz" + +[tools.julia."platforms.macos-x64"] +checksum = "sha256:1a70b7c606d6bac38a246e722369e5b30914dccf9378499d2712fb3bd282642c" +url = "https://julialang-s3.julialang.org/bin/mac/x64/1.12/julia-1.12.6-mac64.tar.gz" + +[tools.julia."platforms.macos-x64-baseline"] +checksum = "sha256:1a70b7c606d6bac38a246e722369e5b30914dccf9378499d2712fb3bd282642c" +url = "https://julialang-s3.julialang.org/bin/mac/x64/1.12/julia-1.12.6-mac64.tar.gz" + +[tools.julia."platforms.windows-x64"] +checksum = "sha256:a63d991976e6893f508c512e3dc7bca1836c1a1f6ad1f3e4aedec159b6733e89" +url = "https://julialang-s3.julialang.org/bin/winnt/x64/1.12/julia-1.12.6-win64.zip" + +[tools.julia."platforms.windows-x64-baseline"] +checksum = "sha256:a63d991976e6893f508c512e3dc7bca1836c1a1f6ad1f3e4aedec159b6733e89" +url = "https://julialang-s3.julialang.org/bin/winnt/x64/1.12/julia-1.12.6-win64.zip" + +[[tools.just]] +version = "1.56.0" +backend = "aqua:casey/just" + +[tools.just."platforms.linux-arm64"] +checksum = "sha256:c8c1d656e9f47569ec1ae2bf8779af2621cdeea6bbbba3b0cacd64f951d25e2b" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-aarch64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074960" + +[tools.just."platforms.linux-arm64-musl"] +checksum = "sha256:c8c1d656e9f47569ec1ae2bf8779af2621cdeea6bbbba3b0cacd64f951d25e2b" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-aarch64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074960" + +[tools.just."platforms.linux-x64"] +checksum = "sha256:fa2a8ec1015d9df5330941ade12437488fc40d33f9c9f8cd4eb70a26de11b639" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074624" + +[tools.just."platforms.linux-x64-baseline"] +checksum = "sha256:fa2a8ec1015d9df5330941ade12437488fc40d33f9c9f8cd4eb70a26de11b639" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074624" + +[tools.just."platforms.linux-x64-musl"] +checksum = "sha256:fa2a8ec1015d9df5330941ade12437488fc40d33f9c9f8cd4eb70a26de11b639" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074624" + +[tools.just."platforms.linux-x64-musl-baseline"] +checksum = "sha256:fa2a8ec1015d9df5330941ade12437488fc40d33f9c9f8cd4eb70a26de11b639" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-unknown-linux-musl.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074624" + +[tools.just."platforms.macos-arm64"] +checksum = "sha256:f35798d4bcdc4db020eef7d2853ad98bbfb97a4d29ee695ba042f18e7fedcc11" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-aarch64-apple-darwin.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074635" + +[tools.just."platforms.macos-x64"] +checksum = "sha256:09b35ff6d17023ffae37ce408d1a78a976d9e001cae54b88e238f7f40db9b783" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-apple-darwin.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074650" + +[tools.just."platforms.macos-x64-baseline"] +checksum = "sha256:09b35ff6d17023ffae37ce408d1a78a976d9e001cae54b88e238f7f40db9b783" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-apple-darwin.tar.gz" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472074650" + +[tools.just."platforms.windows-x64"] +checksum = "sha256:804f5b2fe94291d0df38fd8dfc5620afbf3496f8f11c1915b42a87323234f0ba" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-pc-windows-msvc.zip" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472075917" + +[tools.just."platforms.windows-x64-baseline"] +checksum = "sha256:804f5b2fe94291d0df38fd8dfc5620afbf3496f8f11c1915b42a87323234f0ba" +url = "https://github.com/casey/just/releases/download/1.56.0/just-1.56.0-x86_64-pc-windows-msvc.zip" +url_api = "https://api.github.com/repos/casey/just/releases/assets/472075917" + +[[tools.protoc]] +version = "36.2" +backend = "aqua:protocolbuffers/protobuf/protoc" + +[tools.protoc."platforms.linux-arm64"] +checksum = "sha256:8b8f18bd2b30346efbc698dd5a73dd7c805f3ef8380f6dfc95c768f3f1852f6a" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-aarch_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742403" + +[tools.protoc."platforms.linux-arm64-musl"] +checksum = "sha256:8b8f18bd2b30346efbc698dd5a73dd7c805f3ef8380f6dfc95c768f3f1852f6a" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-aarch_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742403" + +[tools.protoc."platforms.linux-x64"] +checksum = "sha256:121f6c7afe1d4d0e3ea6aab9432038599250134cbf4474cb1167d2c7decd4278" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742434" + +[tools.protoc."platforms.linux-x64-baseline"] +checksum = "sha256:121f6c7afe1d4d0e3ea6aab9432038599250134cbf4474cb1167d2c7decd4278" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742434" + +[tools.protoc."platforms.linux-x64-musl"] +checksum = "sha256:121f6c7afe1d4d0e3ea6aab9432038599250134cbf4474cb1167d2c7decd4278" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742434" + +[tools.protoc."platforms.linux-x64-musl-baseline"] +checksum = "sha256:121f6c7afe1d4d0e3ea6aab9432038599250134cbf4474cb1167d2c7decd4278" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-linux-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742434" + +[tools.protoc."platforms.macos-arm64"] +checksum = "sha256:9cd98a532c5c5e0c4161314de0225de27e4c8a323917b6ea7b1b714d3ae23466" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-osx-aarch_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742436" + +[tools.protoc."platforms.macos-x64"] +checksum = "sha256:228cc7add4616cc14ca5e80dee83209d44449a7aee95a914ae748fa374efb078" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-osx-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742448" + +[tools.protoc."platforms.macos-x64-baseline"] +checksum = "sha256:228cc7add4616cc14ca5e80dee83209d44449a7aee95a914ae748fa374efb078" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-osx-x86_64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742448" + +[tools.protoc."platforms.windows-x64"] +checksum = "sha256:f0c128dc0d8492eceece83bb459a4c0e316764b929ffbf1aa416357fd644edd3" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-win64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742465" + +[tools.protoc."platforms.windows-x64-baseline"] +checksum = "sha256:f0c128dc0d8492eceece83bb459a4c0e316764b929ffbf1aa416357fd644edd3" +url = "https://github.com/protocolbuffers/protobuf/releases/download/v36.2/protoc-36.2-win64.zip" +url_api = "https://api.github.com/repos/protocolbuffers/protobuf/releases/assets/570742465" + +[[tools.shellcheck]] +version = "0.11.0" +backend = "aqua:koalaman/shellcheck" + +[tools.shellcheck."platforms.linux-arm64"] +checksum = "sha256:12b331c1d2db6b9eb13cfca64306b1b157a86eb69db83023e261eaa7e7c14588" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.aarch64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056934" + +[tools.shellcheck."platforms.linux-arm64-musl"] +checksum = "sha256:12b331c1d2db6b9eb13cfca64306b1b157a86eb69db83023e261eaa7e7c14588" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.aarch64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056934" + +[tools.shellcheck."platforms.linux-x64"] +checksum = "sha256:8c3be12b05d5c177a04c29e3c78ce89ac86f1595681cab149b65b97c4e227198" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056942" + +[tools.shellcheck."platforms.linux-x64-baseline"] +checksum = "sha256:8c3be12b05d5c177a04c29e3c78ce89ac86f1595681cab149b65b97c4e227198" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056942" + +[tools.shellcheck."platforms.linux-x64-musl"] +checksum = "sha256:8c3be12b05d5c177a04c29e3c78ce89ac86f1595681cab149b65b97c4e227198" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056942" + +[tools.shellcheck."platforms.linux-x64-musl-baseline"] +checksum = "sha256:8c3be12b05d5c177a04c29e3c78ce89ac86f1595681cab149b65b97c4e227198" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.linux.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056942" + +[tools.shellcheck."platforms.macos-arm64"] +checksum = "sha256:56affdd8de5527894dca6dc3d7e0a99a873b0f004d7aabc30ae407d3f48b0a79" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.darwin.aarch64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056932" + +[tools.shellcheck."platforms.macos-x64"] +checksum = "sha256:3c89db4edcab7cf1c27bff178882e0f6f27f7afdf54e859fa041fca10febe4c6" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.darwin.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056930" + +[tools.shellcheck."platforms.macos-x64-baseline"] +checksum = "sha256:3c89db4edcab7cf1c27bff178882e0f6f27f7afdf54e859fa041fca10febe4c6" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.darwin.x86_64.tar.xz" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056930" + +[tools.shellcheck."platforms.windows-x64"] +checksum = "sha256:8a4e35ab0b331c85d73567b12f2a444df187f483e5079ceffa6bda1faa2e740e" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.zip" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056944" + +[tools.shellcheck."platforms.windows-x64-baseline"] +checksum = "sha256:8a4e35ab0b331c85d73567b12f2a444df187f483e5079ceffa6bda1faa2e740e" +url = "https://github.com/koalaman/shellcheck/releases/download/v0.11.0/shellcheck-v0.11.0.zip" +url_api = "https://api.github.com/repos/koalaman/shellcheck/releases/assets/279056944" + +[[tools.yq]] +version = "4.53.3" +backend = "aqua:mikefarah/yq" + +[tools.yq."platforms.linux-arm64"] +checksum = "sha256:578648e463a11c1b6db6010cbf41eafed6bee79466fcffa1bb446672cf7945ea" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_arm64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146727" +provenance = "cosign" + +[tools.yq."platforms.linux-arm64-musl"] +checksum = "sha256:578648e463a11c1b6db6010cbf41eafed6bee79466fcffa1bb446672cf7945ea" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_arm64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146727" +provenance = "cosign" + +[tools.yq."platforms.linux-x64"] +checksum = "sha256:fa52a4e758c63d38299163fbdd1edfb4c4963247918bf9c1c5d31d84789eded4" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146735" +provenance = "cosign" + +[tools.yq."platforms.linux-x64-baseline"] +checksum = "sha256:fa52a4e758c63d38299163fbdd1edfb4c4963247918bf9c1c5d31d84789eded4" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146735" +provenance = "cosign" + +[tools.yq."platforms.linux-x64-musl"] +checksum = "sha256:fa52a4e758c63d38299163fbdd1edfb4c4963247918bf9c1c5d31d84789eded4" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146735" +provenance = "cosign" + +[tools.yq."platforms.linux-x64-musl-baseline"] +checksum = "sha256:fa52a4e758c63d38299163fbdd1edfb4c4963247918bf9c1c5d31d84789eded4" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_linux_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146735" +provenance = "cosign" + +[tools.yq."platforms.macos-arm64"] +checksum = "sha256:b4ba1ecce3c47f00803f4f964de38394326c7a32eb6540616e04fb2935a0f08d" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_darwin_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146744" +provenance = "cosign" + +[tools.yq."platforms.macos-x64"] +checksum = "sha256:b4ba1ecce3c47f00803f4f964de38394326c7a32eb6540616e04fb2935a0f08d" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_darwin_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146744" +provenance = "cosign" + +[tools.yq."platforms.macos-x64-baseline"] +checksum = "sha256:b4ba1ecce3c47f00803f4f964de38394326c7a32eb6540616e04fb2935a0f08d" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_darwin_amd64" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146744" +provenance = "cosign" + +[tools.yq."platforms.windows-x64"] +checksum = "sha256:e279bc506a452eeafcdf364f91a025455e402a8001169083caf01f4b64a544e2" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_windows_amd64.exe" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146721" +provenance = "cosign" + +[tools.yq."platforms.windows-x64-baseline"] +checksum = "sha256:e279bc506a452eeafcdf364f91a025455e402a8001169083caf01f4b64a544e2" +url = "https://github.com/mikefarah/yq/releases/download/v4.53.3/yq_windows_amd64.exe" +url_api = "https://api.github.com/repos/mikefarah/yq/releases/assets/440146721" +provenance = "cosign" + +[[tools.zig]] +version = "0.16.0" +backend = "core:zig" + +[tools.zig."platforms.linux-arm64"] +checksum = "sha256:ea4b09bfb22ec6f6c6ceac57ab63efb6b46e17ab08d21f69f3a48b38e1534f17" +url = "https://ziglang.org/download/0.16.0/zig-aarch64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.linux-arm64-musl"] +checksum = "sha256:ea4b09bfb22ec6f6c6ceac57ab63efb6b46e17ab08d21f69f3a48b38e1534f17" +url = "https://ziglang.org/download/0.16.0/zig-aarch64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.linux-x64"] +checksum = "sha256:70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.linux-x64-baseline"] +checksum = "sha256:70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.linux-x64-musl"] +checksum = "sha256:70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.linux-x64-musl-baseline"] +checksum = "sha256:70e49664a74374b48b51e6f3fdfbf437f6395d42509050588bd49abe52ba3d00" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-linux-0.16.0.tar.xz" + +[tools.zig."platforms.macos-arm64"] +checksum = "sha256:b23d70deaa879b5c2d486ed3316f7eaa53e84acf6fc9cc747de152450d401489" +url = "https://ziglang.org/download/0.16.0/zig-aarch64-macos-0.16.0.tar.xz" + +[tools.zig."platforms.macos-x64"] +checksum = "sha256:0387557ed1877bc6a2e1802c8391953baddba76081876301c522f52977b52ba7" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-macos-0.16.0.tar.xz" + +[tools.zig."platforms.macos-x64-baseline"] +checksum = "sha256:0387557ed1877bc6a2e1802c8391953baddba76081876301c522f52977b52ba7" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-macos-0.16.0.tar.xz" + +[tools.zig."platforms.windows-x64"] +checksum = "sha256:68659eb5f1e4eb1437a722f1dd889c5a322c9954607f5edcf337bc3684a75a7e" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-windows-0.16.0.zip" + +[tools.zig."platforms.windows-x64-baseline"] +checksum = "sha256:68659eb5f1e4eb1437a722f1dd889c5a322c9954607f5edcf337bc3684a75a7e" +url = "https://ziglang.org/download/0.16.0/zig-x86_64-windows-0.16.0.zip" diff --git a/mise.toml b/mise.toml index 6dd983f6..83dc2355 100644 --- a/mise.toml +++ b/mise.toml @@ -1,57 +1,24 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# The toolchain for echidna. Specs are `latest`; mise.lock records the concrete +# version and per-platform checksum of each, so every checkout installs the +# same bits. Refresh both with: mise upgrade && mise lock +# Canon: hyperpolymath/standards 3-practice/provisioning (PROVISIONING-STANDARD §4). +# Estate policy: no python, deno, node/npm/yarn, go, java or make here; the JS +# runtime is bun. +# +# Rust is pinned by rust-toolchain.toml (rustup), not here. Idris2 comes from +# pack, not mise. Chapel has no mise tool; it is optional (--features chapel). + +[settings] +lockfile = true + [tools] -# Language runtimes -node = "latest" -python = "latest" -rust = "latest" -go = "latest" +just = "latest" zig = "latest" -java = "latest" +protoc = "latest" # echidna-grpc build script (tonic-build) +julia = "latest" bun = "latest" -denojs = "latest" - -# Package managers -npm = "latest" -yarn = "latest" -pnpm = "latest" -pip = "latest" -cargo = "latest" -go-task = "latest" - -# Formatting & Linting -gofmt = "latest" -black = "latest" -isort = "latest" -ruff = "latest" -prettier = "latest" -shfmt = "latest" -stylua = "latest" - -# Build tools -cmake = "latest" -make = "latest" -ninja = "latest" - -# Shell tools -git = "latest" -gnu-sed = "latest" -gnu-tar = "latest" -gnu-grep = "latest" - -# Testing -vitest = "latest" -pytest = "latest" -jest = "latest" - -[env] -# Common environment variables -NODE_ENV = "development" -PYTHONDONTWRITEBYTECODE = "1" -PYTHONUNBUFFERED = "1" - -# Task runner alias -[alias] -task = "go-task" -build = "cargo build --release || npm run build || go build" -test = "cargo test || npm test || go test ./..." -lint = "ruff check . || prettier --check . || black --check ." -fmt = "ruff format . || prettier --write . || black ." +shellcheck = "latest" +yq = "latest" # KYAML formatting/checks (standards scripts/kyaml-format.sh) diff --git a/proofs/acl2/README.adoc b/proofs/acl2/README.adoc index 2f2e208f..8de15467 100644 --- a/proofs/acl2/README.adoc +++ b/proofs/acl2/README.adoc @@ -123,7 +123,7 @@ echidna repl --prover acl2 === Resources -* http://www.cs.utexas.edu/users/moore/acl2/[ACL2 Documentation] -* http://www.cs.utexas.edu/users/moore/acl2/tutorial.html[ACL2 Tutorial] -* http://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____HINTS[Proof +* https://www.cs.utexas.edu/users/moore/acl2/[ACL2 Documentation] +* https://acl2.org/doc/?topic=ACL2____ACL2-TUTORIAL[ACL2 Tutorial] +* https://acl2.org/doc/?topic=ACL2____HINTS[Proof Hints Guide] diff --git a/proofs/pvs/README.adoc b/proofs/pvs/README.adoc index 1b539a62..7cdc7aa5 100644 --- a/proofs/pvs/README.adoc +++ b/proofs/pvs/README.adoc @@ -151,8 +151,8 @@ theorem_name: THEOREM === Resources -* http://pvs.csl.sri.com/[PVS Specification and Verification System] -* http://pvs.csl.sri.com/doc/pvs-language-reference.pdf[PVS Language +* https://pvs.csl.sri.com/[PVS Specification and Verification System] +* https://pvs.csl.sri.com/doc/pvs-language-reference.pdf[PVS Language Reference] -* http://pvs.csl.sri.com/doc/pvs-prover-guide.pdf[PVS Prover Guide] -* http://shemesh.larc.nasa.gov/fm/pvs/tutorial/[PVS Tutorial] +* https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf[PVS Prover Guide] +* https://shemesh.larc.nasa.gov/fm/pvs/[PVS Tutorial] diff --git a/rust-toolchain.toml b/rust-toolchain.toml new file mode 100644 index 00000000..649acb4e --- /dev/null +++ b/rust-toolchain.toml @@ -0,0 +1,10 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# Repo-local Rust pin (AGENTS.md §1a: a repo's own pins stay in the repo so it +# builds standalone). Bump deliberately, together with any new clippy fixes. +# crates/echidna-core-creusot carries its own nightly pin for Creusot only. +[toolchain] +channel = "1.99.0" +components = ["rustfmt", "clippy", "llvm-tools-preview"] +profile = "minimal" diff --git a/scripts/install-proof-toolchains.sh b/scripts/install-proof-toolchains.sh index c24d626e..088a8317 100755 --- a/scripts/install-proof-toolchains.sh +++ b/scripts/install-proof-toolchains.sh @@ -17,6 +17,10 @@ LEAN_VERSION="4.13.0" IDRIS2_VERSION="v0.8.0" LEAN_PREFIX="/opt/lean-${LEAN_VERSION}-linux" +# Private scratch dir for downloads (never a predictable shared path); removed on exit. +WORK="$(mktemp -d)" +trap 'rm -rf "$WORK"' EXIT + log() { printf '\033[1;36m[proof-setup]\033[0m %s\n' "$*"; } have() { command -v "$1" >/dev/null 2>&1; } @@ -61,18 +65,18 @@ log "reminder: invoke agda with LC_ALL=C.UTF-8" # ── 3. Lean 4 (pinned tarball; the elan host 403s under the network policy) ─── if [ ! -x "${LEAN_PREFIX}/bin/lean" ]; then log "installing Lean ${LEAN_VERSION}" - curl -fsSL "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" -o /tmp/lean.tar.zst - $SUDO tar --use-compress-program=unzstd -xf /tmp/lean.tar.zst -C /opt + curl -fsSL "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" -o "$WORK/lean.tar.zst" + $SUDO tar --use-compress-program=unzstd -xf "$WORK/lean.tar.zst" -C /opt fi for b in lean lake; do $SUDO ln -sf "${LEAN_PREFIX}/bin/$b" /usr/local/bin/"$b"; done # ── 4. Idris2 0.8.0 (not packaged; bootstrap from source via Chez, ~10 min) ─── if ! have idris2; then log "building Idris2 ${IDRIS2_VERSION} from source — this is the slow step" - curl -fsSL "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VERSION}.tar.gz" -o /tmp/idris2.tar.gz - rm -rf /tmp/idris2-src && mkdir -p /tmp/idris2-src - tar xzf /tmp/idris2.tar.gz -C /tmp/idris2-src --strip-components=1 - ( cd /tmp/idris2-src \ + curl -fsSL "https://github.com/idris-lang/Idris2/archive/refs/tags/${IDRIS2_VERSION}.tar.gz" -o "$WORK/idris2.tar.gz" + mkdir -p "$WORK/idris2-src" + tar xzf "$WORK/idris2.tar.gz" -C "$WORK/idris2-src" --strip-components=1 + ( cd "$WORK/idris2-src" \ && make bootstrap SCHEME=chezscheme \ && $SUDO make install PREFIX=/usr/local \ && $SUDO make install-with-src-libs PREFIX=/usr/local ) diff --git a/scripts/serve-static.js b/scripts/serve-static.js new file mode 100644 index 00000000..a74d6ae6 --- /dev/null +++ b/scripts/serve-static.js @@ -0,0 +1,46 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +// +// serve-static.js — minimal local static file server for the UI shell. +// Replaces the retired `deno run jsr:@std/http/file-server` recipe. +// Usage (from the directory to serve): bun path/to/serve-static.js [port] +// Local development only: binds 127.0.0.1, serves the current directory. + +import { resolve, sep } from "node:path"; + +const root = resolve(process.cwd()); +const port = Number(process.argv[2] ?? "3000"); + +/** + * Map a request URL path to a file under `root`, or null when the path + * escapes `root` or is malformed. "/" maps to index.html. + * @param {string} pathname + * @returns {string | null} + */ +function resolveRequestPath(pathname) { + let decoded; + try { + decoded = decodeURIComponent(pathname); + } catch { + return null; + } + const rel = decoded === "/" ? "index.html" : decoded.replace(/^\/+/, ""); + const full = resolve(root, rel); + return full === root || full.startsWith(root + sep) ? full : null; +} + +Bun.serve({ + hostname: "127.0.0.1", + port, + /** Serve the requested file, 404 when absent, 403 when outside root. */ + async fetch(req) { + const path = resolveRequestPath(new URL(req.url).pathname); + if (path === null) return new Response("forbidden", { status: 403 }); + const file = Bun.file(path); + return (await file.exists()) + ? new Response(file) + : new Response("not found", { status: 404 }); + }, +}); + +console.log(`serving ${root} on http://127.0.0.1:${port}`); diff --git a/src/interfaces/graphql/Cargo.toml b/src/interfaces/graphql/Cargo.toml index 2a7c8243..a3ad5604 100644 --- a/src/interfaces/graphql/Cargo.toml +++ b/src/interfaces/graphql/Cargo.toml @@ -48,7 +48,7 @@ tracing = "0.1" tracing-subscriber = { version = "0.3", features = ["env-filter"] } # UUID generation -uuid = { version = "1.25.0", features = ["v4", "serde"] } +uuid = { version = "1.25.0", features = ["serde"] } # ids are minted by echidna::ids only [dev-dependencies] reqwest = { version = "0.12", features = ["json"] } diff --git a/src/interfaces/graphql/resolvers.rs b/src/interfaces/graphql/resolvers.rs index 5b667129..d9fd3ab0 100644 --- a/src/interfaces/graphql/resolvers.rs +++ b/src/interfaces/graphql/resolvers.rs @@ -494,7 +494,7 @@ impl EchidnaContext { } pub async fn create_session(&self, goal: &str, kind: CoreProverKind) -> anyhow::Result { - let proof_id = uuid::Uuid::new_v4().to_string(); + let proof_id = echidna::ids::new_record_id().to_string(); if self.ffi_initialized { // Use FFI path diff --git a/src/interfaces/grpc/Cargo.toml b/src/interfaces/grpc/Cargo.toml index b4e64213..062227df 100644 --- a/src/interfaces/grpc/Cargo.toml +++ b/src/interfaces/grpc/Cargo.toml @@ -40,7 +40,7 @@ tracing = "0.1" tracing-subscriber = { version = "0.3", features = ["env-filter"] } # UUID -uuid = { version = "1.25.0", features = ["v4", "serde"] } +uuid = { version = "1.25.0", features = ["serde"] } # ids are minted by echidna::ids only # Async trait support async-trait = "0.1" diff --git a/src/interfaces/grpc/ffi_wrapper.rs b/src/interfaces/grpc/ffi_wrapper.rs index 7c030faa..487e19d0 100644 --- a/src/interfaces/grpc/ffi_wrapper.rs +++ b/src/interfaces/grpc/ffi_wrapper.rs @@ -8,8 +8,10 @@ use std::os::raw::c_int; // External Zig FFI functions (from libechidna_ffi.so) extern "C" { pub fn echidna_init() -> c_int; + #[allow(dead_code)] // mirrors the Zig FFI export; no gRPC handler calls it yet pub fn echidna_deinit(); pub fn echidna_create_prover(kind: u8) -> c_int; + #[allow(dead_code)] // mirrors the Zig FFI export; no gRPC handler calls it yet pub fn echidna_destroy_prover(handle: c_int); pub fn echidna_parse_string(handle: c_int, content: *const u8, len: usize) -> c_int; pub fn echidna_verify_proof(handle: c_int) -> c_int; @@ -81,6 +83,7 @@ pub fn create_prover(prover_kind: u8) -> Result { } /// Destroy a prover instance +#[allow(dead_code)] // mirrors the Zig FFI export; no gRPC handler calls it yet pub fn destroy_prover(handle: i32) -> Result<()> { unsafe { echidna_destroy_prover(handle); @@ -210,6 +213,7 @@ pub fn proto_kind_to_ffi(kind: i32) -> Result { } /// Convert FFI ordinal to gRPC ProverKind +#[allow(dead_code)] // mirrors the Zig FFI export; no gRPC handler calls it yet pub fn ffi_to_proto_kind(ordinal: u8) -> i32 { match ordinal { 0 => 1, // Agda diff --git a/src/interfaces/grpc/main.rs b/src/interfaces/grpc/main.rs index ac2fdde9..f9f9c81f 100644 --- a/src/interfaces/grpc/main.rs +++ b/src/interfaces/grpc/main.rs @@ -179,7 +179,7 @@ impl ProofService for ProofServiceImpl { let core_kind = proto_kind_to_core(req.prover) .ok_or_else(|| Status::invalid_argument("Unknown prover kind"))?; - let proof_id = uuid::Uuid::new_v4().to_string(); + let proof_id = echidna::ids::new_record_id().to_string(); // Try FFI path first if available if self.ffi_initialized { diff --git a/src/interfaces/rest/Cargo.toml b/src/interfaces/rest/Cargo.toml index 708afaec..f8195993 100644 --- a/src/interfaces/rest/Cargo.toml +++ b/src/interfaces/rest/Cargo.toml @@ -36,11 +36,11 @@ tracing = "0.1" tracing-subscriber = { version = "0.3", features = ["env-filter"] } # UUID -uuid = { version = "1.25.0", features = ["v4", "serde"] } +uuid = { version = "1.25.0", features = ["serde"] } # ids are minted by echidna::ids only # OpenAPI utoipa = { version = "6.0", features = ["axum_extras"] } -utoipa-swagger-ui = { version = "9.0", features = ["axum"] } +utoipa-swagger-ui = { version = "10.0", features = ["axum"] } # ECHIDNA core echidna = { path = "../../.." } diff --git a/src/interfaces/rest/handlers.rs b/src/interfaces/rest/handlers.rs index 200c8207..5d75d7b0 100644 --- a/src/interfaces/rest/handlers.rs +++ b/src/interfaces/rest/handlers.rs @@ -194,7 +194,7 @@ pub async fn submit_proof( let prover = ProverFactory::create(core_kind, config) .map_err(|e| (StatusCode::BAD_REQUEST, e.to_string()))?; - let proof_id = uuid::Uuid::new_v4().to_string(); + let proof_id = echidna::ids::new_record_id().to_string(); // Parse the goal let proof_state = prover diff --git a/src/rust/dispatch.rs b/src/rust/dispatch.rs index 4008a731..170aafe0 100644 --- a/src/rust/dispatch.rs +++ b/src/rust/dispatch.rs @@ -1160,7 +1160,7 @@ fn build_proof_attempt( let started_at = now - chrono::Duration::milliseconds(duration_ms as i64); ProofAttempt { - attempt_id: uuid::Uuid::new_v4().to_string(), + attempt_id: crate::ids::new_record_id().to_string(), obligation_id, repo: String::new(), file: String::new(), diff --git a/src/rust/ids.rs b/src/rust/ids.rs new file mode 100644 index 00000000..c1775cdb --- /dev/null +++ b/src/rust/ids.rs @@ -0,0 +1,144 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The single place echidna mints identifiers. +//! +//! Every UUID echidna creates comes from one of the functions here; no other +//! module calls `Uuid::new_v4`/`Uuid::now_v7` directly. There are two kinds: +//! +//! * [`new_record_id`] — a **UUIDv7** (RFC 9562 §5.7) for things that +//! *happen*: proof requests, sessions, attempts, runs, findings. v7 is +//! time-ordered, so ids sort by creation time. Within one process the `uuid` +//! crate's shared v7 context makes successive ids strictly increasing. +//! This is the estate default (standards `docs/UUID-V7-ESTATE-STANDARD.adoc`). +//! * [`content_id`] — a **UUIDv8** (RFC 9562 §5.8, Appendix B.2 hash-based +//! layout) for things that *are*: proof goals, prove results, corpus +//! entries, octads. The id is derived from the value alone, so equal content +//! always gets the same id, wherever and whenever it is computed: +//! +//! 1. canonicalise the value with JCS (RFC 8785); +//! 2. SHA-256 the canonical bytes; +//! 3. take the first 16 bytes of the digest; +//! 4. set the version nibble to `8` and the variant bits to `10`. +//! +//! The v8 layout is an owner decision of 2026-10-05; the estate v7 standard +//! defines no v8 layout yet, so this module is where it is written down. +//! +//! [`temp_token`] is for throwaway temp-file names only. It is a v7 in simple +//! (hyphen-free) form and never leaves the machine. + +use serde::Serialize; +use sha2::{Digest, Sha256}; +use uuid::Uuid; + +/// Mint a fresh time-ordered record id (UUIDv7) for an event or record: +/// a proof request, session, attempt, run or finding. +pub fn new_record_id() -> Uuid { + Uuid::now_v7() +} + +/// Derive the deterministic content id (UUIDv8, SHA-256 over the JCS form) +/// of a serialisable value: a proof goal, prove result, corpus entry or octad. +/// +/// Two values with the same JCS canonical form always get the same id. +/// Fails only when the value cannot be represented as JSON (for example a +/// map with non-string keys or a non-finite float). +pub fn content_id(value: &T) -> Result { + let canonical = serde_json_canonicalizer::to_vec(value)?; + Ok(content_id_from_canonical_bytes(&canonical)) +} + +/// Derive the UUIDv8 content id from bytes that are already JCS-canonical. +/// +/// Callers holding canonical bytes (for example the stdout of a JCS emitter) +/// use this to avoid a re-serialisation; [`content_id`] calls it too. +pub fn content_id_from_canonical_bytes(canonical: &[u8]) -> Uuid { + let digest = Sha256::digest(canonical); + let mut bytes = [0u8; 16]; + bytes.copy_from_slice(&digest[..16]); + // `new_v8` sets the version nibble to 8 and the variant bits to 0b10. + Uuid::new_v8(bytes) +} + +/// Return a unique, filesystem-safe token for a temp-file name. +/// +/// Not an identifier of anything: it only keeps concurrent prover +/// invocations from colliding in the temp directory. +pub fn temp_token() -> String { + new_record_id().simple().to_string() +} + +#[cfg(test)] +mod tests { + use super::*; + use serde_json::json; + + #[test] + fn record_id_is_v7_with_rfc_variant() { + let id = new_record_id(); + assert_eq!(id.get_version_num(), 7); + assert_eq!(id.get_variant(), uuid::Variant::RFC4122); + } + + #[test] + fn record_ids_are_strictly_monotonic_in_process() { + let ids: Vec = (0..10_000).map(|_| new_record_id()).collect(); + for pair in ids.windows(2) { + assert!(pair[0] < pair[1], "{} !< {}", pair[0], pair[1]); + } + } + + #[test] + fn content_id_is_v8_with_rfc_variant() { + let id = content_id(&json!({"goal": "forall n, n + 0 = n"})).unwrap(); + assert_eq!(id.get_version_num(), 8); + assert_eq!(id.get_variant(), uuid::Variant::RFC4122); + // Variant bits 10 in the top of byte 8; version 8 in byte 6. + let b = id.as_bytes(); + assert_eq!(b[6] >> 4, 0x8); + assert_eq!(b[8] >> 6, 0b10); + } + + #[test] + fn same_jcs_content_gives_same_id() { + // Key order and whitespace differ; the JCS form is identical. + let a: serde_json::Value = + serde_json::from_str(r#"{"prover":"lean","goal":"p","n":1.0}"#).unwrap(); + let b: serde_json::Value = + serde_json::from_str(r#"{ "n": 1, "goal": "p", "prover": "lean" }"#).unwrap(); + assert_eq!(content_id(&a).unwrap(), content_id(&b).unwrap()); + } + + #[test] + fn different_content_gives_different_id() { + let a = content_id(&json!({"goal": "p"})).unwrap(); + let b = content_id(&json!({"goal": "q"})).unwrap(); + assert_ne!(a, b); + } + + #[test] + fn content_id_matches_documented_construction() { + // Planted positive control: recompute the layout by hand. + let canonical = br#"{"a":1,"b":[true,null]}"#; + let value = json!({"b": [true, null], "a": 1}); + assert_eq!( + serde_json_canonicalizer::to_vec(&value).unwrap(), + canonical.to_vec() + ); + let digest = Sha256::digest(canonical); + let mut expect = [0u8; 16]; + expect.copy_from_slice(&digest[..16]); + expect[6] = (expect[6] & 0x0f) | 0x80; + expect[8] = (expect[8] & 0x3f) | 0x80; + assert_eq!(content_id(&value).unwrap(), Uuid::from_bytes(expect)); + } + + #[test] + fn temp_token_is_hyphen_free_and_unique() { + let a = temp_token(); + let b = temp_token(); + assert_eq!(a.len(), 32); + assert!(!a.contains('-')); + assert_ne!(a, b); + } +} diff --git a/src/rust/integration.rs b/src/rust/integration.rs index 658a8ef6..7a69ff65 100644 --- a/src/rust/integration.rs +++ b/src/rust/integration.rs @@ -142,7 +142,7 @@ impl IntegrationService { backend: Box, ) -> Result { // Generate unique session ID - let session_id = uuid::Uuid::new_v4().to_string(); + let session_id = crate::ids::new_record_id().to_string(); // Create initial proof state let goal = Goal { diff --git a/src/rust/lib.rs b/src/rust/lib.rs index c927b4f5..987d1af1 100644 --- a/src/rust/lib.rs +++ b/src/rust/lib.rs @@ -26,6 +26,7 @@ pub mod fault_tolerance; // Circuit breakers, retries, bulkheads pub mod ffi; pub mod gnn; // Graph Neural Network integration for proof search guidance pub mod groove; // Gossamer Groove discovery endpoint (port 9000) +pub mod ids; // The single ID-minting module: UUIDv7 record ids, UUIDv8 content ids pub mod integrity; pub mod ipc; // L1: Cap'n Proto IPC transport (UDS primary, TCP fallback) pub mod learning; // Continuous self-learning loop (MCTS + self-play + curriculum + daemon) diff --git a/src/rust/provers/acl2.rs b/src/rust/provers/acl2.rs index 666e6356..08c31e77 100644 --- a/src/rust/provers/acl2.rs +++ b/src/rust/provers/acl2.rs @@ -1337,10 +1337,7 @@ impl ProverBackend for ACL2Backend { // Generate defthm with hint let defthm = self.generate_defthm( - &format!( - "echidna_goal_{}", - uuid::Uuid::new_v4().to_string().replace('-', "") - ), + &format!("echidna_goal_{}", crate::ids::temp_token()), &goal.target, &[hint], ); @@ -1391,8 +1388,10 @@ impl ProverBackend for ACL2Backend { if let Some(p) = state.metadata.get("source_path").and_then(|v| v.as_str()) { Some(PathBuf::from(p)) } else if let Some(src) = state.metadata.get("acl2_source").and_then(|v| v.as_str()) { - let tmp = std::env::temp_dir() - .join(format!("echidna_acl2_verify_{}.lisp", uuid::Uuid::new_v4())); + let tmp = std::env::temp_dir().join(format!( + "echidna_acl2_verify_{}.lisp", + crate::ids::temp_token() + )); tokio::fs::write(&tmp, src) .await .context("Failed to write temp file")?; @@ -1426,8 +1425,10 @@ impl ProverBackend for ACL2Backend { let content = self.export(state).await?; // Write to temp file - let temp_file = - std::env::temp_dir().join(format!("echidna_acl2_verify_{}.lisp", uuid::Uuid::new_v4())); + let temp_file = std::env::temp_dir().join(format!( + "echidna_acl2_verify_{}.lisp", + crate::ids::temp_token() + )); tokio::fs::write(&temp_file, &content) .await diff --git a/src/rust/provers/agda.rs b/src/rust/provers/agda.rs index aaefc3ef..55af5691 100644 --- a/src/rust/provers/agda.rs +++ b/src/rust/provers/agda.rs @@ -382,8 +382,10 @@ impl ProverBackend for AgdaBackend { return Ok(output.status.success()); } if let Some(source) = state.metadata.get("agda_source").and_then(|v| v.as_str()) { - let temp_file = std::env::temp_dir() - .join(format!("echidna_agda_verify_{}.agda", uuid::Uuid::new_v4())); + let temp_file = std::env::temp_dir().join(format!( + "echidna_agda_verify_{}.agda", + crate::ids::temp_token() + )); tokio::fs::write(&temp_file, source).await?; let mut cmd = Command::new(&self.config.executable); if let Some(parent) = temp_file.parent() { diff --git a/src/rust/provers/altergo.rs b/src/rust/provers/altergo.rs index 8c9053b9..2f887be7 100644 --- a/src/rust/provers/altergo.rs +++ b/src/rust/provers/altergo.rs @@ -175,7 +175,7 @@ impl ProverBackend for AltErgoBackend { .and_then(|v| v.as_str()) { let tmp = std::env::temp_dir() - .join(format!("echidna_altergo_{}.ae", uuid::Uuid::new_v4())); + .join(format!("echidna_altergo_{}.ae", crate::ids::temp_token())); tokio::fs::write(&tmp, src) .await .context("Failed to write temp file")?; diff --git a/src/rust/provers/coq.rs b/src/rust/provers/coq.rs index 84645195..4eaa6784 100644 --- a/src/rust/provers/coq.rs +++ b/src/rust/provers/coq.rs @@ -945,10 +945,8 @@ impl ProverBackend for CoqBackend { return Ok(output.status.success()); } if let Some(source) = state.metadata.get("coq_source").and_then(|v| v.as_str()) { - let temp_file = std::env::temp_dir().join(format!( - "echidna_coq_verify_{}.v", - uuid::Uuid::new_v4().simple() - )); + let temp_file = std::env::temp_dir() + .join(format!("echidna_coq_verify_{}.v", crate::ids::temp_token())); tokio::fs::write(&temp_file, source) .await .context("Failed to write temp file")?; diff --git a/src/rust/provers/cvc5.rs b/src/rust/provers/cvc5.rs index 1d1682bb..dd8a14c8 100644 --- a/src/rust/provers/cvc5.rs +++ b/src/rust/provers/cvc5.rs @@ -20,7 +20,6 @@ use std::path::PathBuf; use std::process::{Child, Command, Stdio}; use std::sync::{Arc, Mutex}; use tokio::fs; -use uuid::Uuid; use crate::core::{Goal, ProofState, Tactic, TacticResult, Term}; use crate::provers::{ProverBackend, ProverConfig, ProverKind}; @@ -637,8 +636,10 @@ impl ProverBackend for CVC5Backend { s }; - let temp_file = - std::env::temp_dir().join(format!("echidna_cvc5_verify_{}.smt2", Uuid::new_v4())); + let temp_file = std::env::temp_dir().join(format!( + "echidna_cvc5_verify_{}.smt2", + crate::ids::temp_token() + )); fs::write(&temp_file, commands) .await .context("Failed to write CVC5 temp file")?; diff --git a/src/rust/provers/dafny.rs b/src/rust/provers/dafny.rs index 6a5a7a65..3f10468d 100644 --- a/src/rust/provers/dafny.rs +++ b/src/rust/provers/dafny.rs @@ -20,8 +20,7 @@ impl DafnyBackend { /// Generate a minimal valid Dafny program with assertions for the goal and axioms. fn to_input_format(&self, state: &ProofState) -> Result { - let mut s = - String::from("// SPDX-License-Identifier: MPL-2.0\nmethod EchidnaGoal() {\n"); + let mut s = String::from("// SPDX-License-Identifier: MPL-2.0\nmethod EchidnaGoal() {\n"); // Add axioms as assume statements for (i, ax) in state.context.axioms.iter().enumerate() { diff --git a/src/rust/provers/hol_light.rs b/src/rust/provers/hol_light.rs index 2aff72f6..27de8e9b 100644 --- a/src/rust/provers/hol_light.rs +++ b/src/rust/provers/hol_light.rs @@ -552,7 +552,7 @@ impl ProverBackend for HolLightBackend { .and_then(|v| v.as_str()) { let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_{}.ml", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_{}.ml", crate::ids::temp_token())); fs::write(&temp_file, source).await?; let load_cmd = format!("#use \"{}\";;", temp_file.display()); let result = self.execute_command(&load_cmd).await; @@ -577,7 +577,7 @@ impl ProverBackend for HolLightBackend { // Write to temporary file let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_{}.ml", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_{}.ml", crate::ids::temp_token())); fs::write(&temp_file, hol_content).await?; diff --git a/src/rust/provers/idris2.rs b/src/rust/provers/idris2.rs index 2d6f91be..8b0fcac3 100644 --- a/src/rust/provers/idris2.rs +++ b/src/rust/provers/idris2.rs @@ -807,7 +807,7 @@ impl ProverBackend for Idris2Backend { } if let Some(source) = state.metadata.get("idris2_source").and_then(|v| v.as_str()) { let temp_dir = - std::env::temp_dir().join(format!("echidna_idris2_{}", uuid::Uuid::new_v4())); + std::env::temp_dir().join(format!("echidna_idris2_{}", crate::ids::temp_token())); tokio::fs::create_dir_all(&temp_dir).await?; let temp_file = temp_dir.join("Verify.idr"); tokio::fs::write(&temp_file, source).await?; diff --git a/src/rust/provers/isabelle.rs b/src/rust/provers/isabelle.rs index 4e640ac0..f6363031 100644 --- a/src/rust/provers/isabelle.rs +++ b/src/rust/provers/isabelle.rs @@ -177,11 +177,13 @@ fn build_isabelle_temp_dir(tag: &str) -> Result { /// /// Isabelle ROOT files declare sessions like: /// -/// session Tropical_Semirings in "." = "HOL-Library" + -/// theories -/// Tropical_v2 -/// Tropical_Kleene -/// ... +/// ```text +/// session Tropical_Semirings in "." = "HOL-Library" + +/// theories +/// Tropical_v2 +/// Tropical_Kleene +/// ... +/// ``` /// /// When a probe theory is going to do `imports Tropical_v2`, the temp /// probe session needs to inherit from the session that owns diff --git a/src/rust/provers/lean.rs b/src/rust/provers/lean.rs index c8d8443a..99ea788b 100644 --- a/src/rust/provers/lean.rs +++ b/src/rust/provers/lean.rs @@ -1198,7 +1198,7 @@ impl ProverBackend for LeanBackend { // Create a temporary file and check it with Lean let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_lean_{}.lean", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_lean_{}.lean", crate::ids::temp_token())); tokio::fs::write(&temp_file, content) .await @@ -1268,7 +1268,7 @@ impl ProverBackend for LeanBackend { // Write to temp file and check let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_tactic_{}.lean", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_tactic_{}.lean", crate::ids::temp_token())); tokio::fs::write(&temp_file, &lean_code) .await @@ -1327,8 +1327,10 @@ impl ProverBackend for LeanBackend { }; } if let Some(source) = state.metadata.get("lean_source").and_then(|v| v.as_str()) { - let temp_file = std::env::temp_dir() - .join(format!("echidna_lean_verify_{}.lean", uuid::Uuid::new_v4())); + let temp_file = std::env::temp_dir().join(format!( + "echidna_lean_verify_{}.lean", + crate::ids::temp_token() + )); tokio::fs::write(&temp_file, source) .await .context("Failed to write temporary file")?; @@ -1351,7 +1353,7 @@ impl ProverBackend for LeanBackend { // Write to temp file and check with Lean let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_verify_{}.lean", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_verify_{}.lean", crate::ids::temp_token())); tokio::fs::write(&temp_file, &lean_code) .await @@ -1540,7 +1542,7 @@ impl ProverBackend for LeanBackend { let search_code = format!("#check @{}\n", pattern.replace('*', "_")); let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_search_{}.lean", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_search_{}.lean", crate::ids::temp_token())); tokio::fs::write(&temp_file, &search_code) .await diff --git a/src/rust/provers/mizar.rs b/src/rust/provers/mizar.rs index c93cc9c7..3b5025aa 100644 --- a/src/rust/provers/mizar.rs +++ b/src/rust/provers/mizar.rs @@ -564,7 +564,7 @@ impl ProverBackend for MizarBackend { if let Some(source) = state.metadata.get("mizar_source").and_then(|v| v.as_str()) { let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_{}.miz", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_{}.miz", crate::ids::temp_token())); let mut file = fs::File::create(&temp_file).await?; file.write_all(source.as_bytes()).await?; file.sync_all().await?; @@ -581,7 +581,7 @@ impl ProverBackend for MizarBackend { let mizar_content = self.export_to_mizar(state)?; let temp_dir = std::env::temp_dir(); - let temp_file = temp_dir.join(format!("echidna_{}.miz", uuid::Uuid::new_v4())); + let temp_file = temp_dir.join(format!("echidna_{}.miz", crate::ids::temp_token())); let mut file = fs::File::create(&temp_file).await?; file.write_all(mizar_content.as_bytes()).await?; diff --git a/src/rust/provers/spass.rs b/src/rust/provers/spass.rs index 04024def..7e98a7bf 100644 --- a/src/rust/provers/spass.rs +++ b/src/rust/provers/spass.rs @@ -187,7 +187,7 @@ impl ProverBackend for SPASSBackend { .map(Ok) .unwrap_or_else(|| self.to_dfg(state))?; let tmp = std::env::temp_dir() - .join(format!("echidna_spass_{}.dfg", uuid::Uuid::new_v4())); + .join(format!("echidna_spass_{}.dfg", crate::ids::temp_token())); tokio::fs::write(&tmp, dfg_code).await?; tmp }; diff --git a/src/rust/server.rs b/src/rust/server.rs index e55981a4..c62a6a97 100644 --- a/src/rust/server.rs +++ b/src/rust/server.rs @@ -295,7 +295,7 @@ async fn agent_plan_handler( use echidna::agent::Priority; let goal = AgenticGoal { goal: Goal { - id: uuid::Uuid::new_v4().to_string(), + id: echidna::ids::new_record_id().to_string(), target: Term::Const("?".to_string()), hypotheses: vec![], }, @@ -1066,7 +1066,7 @@ async fn create_session( .map_err(|e| AppError::InternalError(e.to_string()))?; // Create session - let session_id = uuid::Uuid::new_v4().to_string(); + let session_id = echidna::ids::new_record_id().to_string(); let session = ProofSession { prover, state: None, diff --git a/src/rust/verification/mod.rs b/src/rust/verification/mod.rs index c7ef3bdb..728c347a 100644 --- a/src/rust/verification/mod.rs +++ b/src/rust/verification/mod.rs @@ -27,7 +27,7 @@ //! pluggable tiebreak. //! //! Picking between them: see the "Guide: Picking an arbitration -//! mechanism" entry in `docs/wiki/Guides.md`. +//! mechanism" entry in `docs/wikis/Guides.md`. //! //! Unified entry point: `result_arbiter` adapts per-prover //! [`crate::provers::outcome::ProverOutcome`]s into whichever mechanism diff --git a/src/rust/verification/result_arbiter.rs b/src/rust/verification/result_arbiter.rs index 6a442418..4c9702e6 100644 --- a/src/rust/verification/result_arbiter.rs +++ b/src/rust/verification/result_arbiter.rs @@ -60,7 +60,7 @@ impl ProverAttempt { /// Which fusion mechanism decides the verdict. /// -/// See "Guide: Picking an arbitration mechanism" in `docs/wiki/Guides.md`. +/// See "Guide: Picking an arbitration mechanism" in `docs/wikis/Guides.md`. #[derive(Debug, Clone, Copy, PartialEq, Default, Serialize, Deserialize)] #[serde(tag = "mechanism", rename_all = "snake_case")] pub enum ArbitrationPolicy { diff --git a/test.txt b/test.txt deleted file mode 100644 index a72b7b4c..00000000 --- a/test.txt +++ /dev/null @@ -1 +0,0 @@ -Test GPG signing diff --git a/tests/s4_loop_closure.rs b/tests/s4_loop_closure.rs index f5be019e..bcc8851c 100644 --- a/tests/s4_loop_closure.rs +++ b/tests/s4_loop_closure.rs @@ -38,10 +38,10 @@ use echidna::verisim_bridge::{prover_kind_to_str, ProofAttempt, VeriSimDBClient} fn fresh_attempt(obligation_class: &str, prover: ProverKind, outcome: &str) -> ProofAttempt { let now = chrono::Utc::now(); ProofAttempt { - attempt_id: uuid::Uuid::new_v4().to_string(), + attempt_id: echidna::ids::new_record_id().to_string(), // Tag the obligation_id with the test name so we can find our own // rows even if other tests are writing concurrently. - obligation_id: format!("test-s4-loop-{}", uuid::Uuid::new_v4()), + obligation_id: format!("test-s4-loop-{}", echidna::ids::temp_token()), repo: "hyperpolymath/echidna".to_string(), file: "tests/s4_loop_closure.rs".to_string(), claim: "true".to_string(), @@ -124,7 +124,7 @@ async fn s4_class_aggregation_visible_in_mv() -> Result<()> { // table. The test passes whether or not it sees its own writes — the // contract is that the MV endpoint responds and the response shape // is parseable. - let unique_class = format!("test-mv-{}", uuid::Uuid::new_v4()); + let unique_class = format!("test-mv-{}", echidna::ids::temp_token()); // Seed a few attempts so the MV has something to aggregate. for outcome in ["success", "success", "failure"] {