Repository navigation
chore: echidna first-run start point (CI restore, drift, ids, template form) - #407
Merged
Merged
Conversation
- actions.lock: refresh with `gh actions-lock` after dependabot #405 bumped codeql-action v4.38.2, haskell-actions/setup v2.12.1 and taiki-e/install-action v2.87.22 without updating the lock (#401). The SHA-keyed entries the tool drops in write mode are kept. `gh actions-lock --no-fix` is clean. - rust-native-reusable.yml: SHA-pin the callee's actions. The repo sets sha_pinning_required, and GitHub does not resolve tag refs through actions.lock inside a local reusable workflow, so every Rust CI run since 2026-07 ended in startup_failure ("actions ... are not allowed"). - src/interfaces/rest/Cargo.toml: utoipa-swagger-ui 9.0 -> 10.0. The dependabot #404 lockfile bump landed without its manifest change, so `cargo check --locked` refused the lock. - cargo fmt: dafny.rs line shortened by the #406 licence rewrite. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
echidna#314. Of 352 baseline entries, 296 matched no finding from the current scanner (hypatia main after #883, tokenless scan at --severity medium, the same inputs as the governance baseline job). They described files and rules that no longer exist, which made the baseline read as far more accepted risk than echidna carries. The 56 live entries are kept unchanged (notes preserved) and now carry tracking_issue #314 so they burn down against it. Checked with standards scripts/apply-baseline.sh (blocking mode): old and new baselines suppress the same 68 findings and keep the same 52 (27 medium, 25 warn). All 27 high findings stay acknowledged. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01QFphKkDVB9pUDSCD4bkz65
… content) All 28 former `Uuid::new_v4()` call sites now go through one module, src/rust/ids.rs: - new_record_id(): UUIDv7 for proof requests, sessions, attempts and runs (REST, gRPC, GraphQL, server, dispatch, s4 loop test). - temp_token(): hyphen-free v7 for prover temp-file names. - content_id(value): UUIDv8 per RFC 9562 Appendix B.2 - SHA-256 over the JCS (RFC 8785) bytes, first 16 bytes, version 8, variant 10. Implemented and tested, not yet used for goals/corpus/octads (stored identity hashes need their own migration). JCS comes from the public serde_json_canonicalizer crate; the estate ijson-jcs crate is private on GitHub, so a public build cannot use it. uuid features: v7+v8 at the root; the interface crates drop v4. Tests: v7 version/variant, 10k strictly monotonic ids, v8 version/variant bits, same-JCS-content -> same id, and a hand-recomputed planted control. ADR: docs/decisions/2026-10-05-id-minting.adoc. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Descriptor drift - META.a2ml aligned with STATE.a2ml (2.3.0; secondary deps Chapel/Bun/Guix); echidnabot directive no longer claims "113 prover backends". - CODEOWNERS: src/rust/core.rs (missing) -> src/rust/lib.rs. - .echidnabot.toml: ipkg path -> src/abi/echidnaabi.ipkg (the file that exists). - Cargo workspace: drop dead `echidnabot` exclude (deleted 2026-04). - settings.yml: KYAML; rebase merge off; wiki on; classic branch-protection block removed (rulesets are the source of truth; it named contexts no workflow reports). - dependabot.yml: KYAML; npm block removed (no package.json); codeql-action hold; cargo security-only. - echidna-core-spark -> echidna-core-creusot, documented as Creusot with annotations STATED, NOT PROVED; the Creusot job is workflow_dispatch-only instead of a red check on every push. - 6a2/ -> descriptiles/ for echidna-playground and HOL-o-extension, and the dust/must/trust contractile write destinations (DEBT D7 resolved). - SECURITY.md duplicate -> .github/SECURITY.md pointer; links fixed. Reproducibility - rust-toolchain.toml (1.99.0); mise.toml rewritten to the provisioning standard (latest + mise.lock; no python/deno/node/go/java; adds protoc for the gRPC build script); mise.lock added. - Deno removed: deno.lock, web-project-deno.json, k9iser deno source; the serve-ui/gui recipes use scripts/serve-static.js under Bun (binds 127.0.0.1, refuses path traversal). - wolfi-base pinned by digest in Containerfile and container/Containerfile. - Julia Project.toml: real UUID (v4, Julia ecosystem convention). - test.txt and the invalid .gitlab-ci.yml removed. CI and tests - Two doctests that never compiled (isabelle.rs ROOT example, echidna-core TypeInfo crate path) fixed: `cargo test --workspace --locked` passes. - gRPC ffi_wrapper: dead-code allows on FFI mirrors so clippy -D warnings passes. - echidna-mcp: rmcp 3.5 ServerInfo -> ServerConfig; capnpc 0.27 to match capnp 0.27. - static-analysis-gate.yml from rsr-template-repo (panic-attack assail + hypatia), recorded in actions.lock; `gh actions-lock --no-fix` clean. Community health - .github: SUPPORT.md, pull_request_template.md, ISSUE_TEMPLATE (KYAML), copilot-instructions.md, rulesets/ payloads (not applied); duplicate lowercase funding.yml (wrong account) removed. Wiki - docs/wiki -> docs/wikis (template path); Home gains an honest capability table (implemented / wired / tested / CI-gated / proved / deployed). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
|
Important Review skippedToo many files! This PR contains 117 files, which is 17 over the limit of 100. To get a review, reduce the PR to 100 files or fewer by splitting it into smaller PRs or changing its base branch. Upgrade to a paid plan to raise the limit. This review couldn't start because sufficient usage credits or metered capacity aren't available. Add credits or update usage-based reviews in the billing tab, then retry. ⚙️ Run configuration
⛔ Files ignored due to path filters (4)
📒 Files selected for processing (117)
You can disable this status message by setting the
Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out. Comment |
![github-advanced-security[bot]](https://avatars.githubusercontent.com/in/57789?s=60&v=4){kind=small}
- rust-ci.yml: inline the former local reusable rust-native-reusable.yml. Calling it still ended in a zero-job "workflow file issue" on PR #407 (with SHA refs, actionlint clean, actions-lock clean) while plain workflows started normally. Job names keep the canonical `rust-ci / ...` contexts. actions.lock refreshed with gh actions-lock. - Cargo.lock: rustls 0.23.40 -> 0.23.45 (RUSTSEC-2026-0285, Cargo audit red). - Hypatia findings: HTTPS for prover links in docs (dead mizar 8.1.14 and ACL2/PVS tutorial links repointed); fabricated codeql-action/trufflehog SHAs in echidna-playground workflows replaced with real ones; Copilot agent uses bunx, not npx; template references to src/interface/ point at echidna's src/abi/ and ffi/zig/; static-analysis-gate annotation steps no longer swallow failures with `|| true`. - .hypatia-baseline.json: the 15 remaining pre-existing workflow-hardening findings (harden-runner, container tag pins, secrets: inherit, two masked-exit steps) and the tombstone doc grandfathered under #314, as that issue prescribes, so the gate fails only on new findings. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…wording) - scripts/install-proof-toolchains.sh: downloads and the Idris2 source tree go to a mktemp -d dir removed on exit, not fixed paths under /tmp (CWE-377, hypatia hardcoded_tmp). - copilot-instructions.md / coding-agent.yml: wording no longer trips the SD022 and npx patterns. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
3 tasks
hyperpolymath
added a commit
that referenced
this pull request
Oct 5, 2026
… CI (#409) Follow-up to #407 (merged as b97a799), so this PR is based on `main`, not stacked. ## What this does **1. `echidna prove --output json`** implements the shared `echidna.prove.result/1` contract. - stdout carries exactly one JCS-canonical (RFC 8785) I-JSON object; logs go to stderr. - `status` comes from `ProverOutcome::prove_status`: `Proved` → `verified`, `NoProofFound` → `failed`, `Timeout` → `timeout`, `InconsistentPremises` → `unknown`, and input, prover or system failures → `error`. Failures before the check (no backend, unreadable file, parse error) are also `error` objects. - Exit code is 0 iff `verified`. - `trust.confidence` is `null` unless a receipt backs it. This is the epistemic-types receipt/warrant pattern, used as a pattern only, not as a dependency. This path checks no certificate, so the value is always `null`. `trust.axioms` comes from ECHIDNA's axiom tracker. - Human output is still the default and unchanged. - Docs: `docs/PROVE-RESULT-CONTRACT.adoc`. **2. `echidna-core` 0.2.0 can now be used by clients** such as echidnabot and proof-burrower. - `ProverKind` moved into the crate. `echidna::ProverKind` and `echidna::provers::ProverKind` re-export it, so no ECHIDNA source changed. - Adds `prove_result` (the contract type, a JCS serialiser and a strict parser). - Adds `trust`, a re-export of the `echidna-core-creusot` trust kernel that echidnabot already pins. - The git-dependency recipe and the stability policy are in `crates/echidna-core/README.adoc`. **3. Zig FFI and the unified-api-adapter check.** - `ffi/zig` did not compile on any Zig release (0.14.1, 0.15.2 and 0.16.0 all failed) and no workflow built it. - It now compiles in pure Zig (opaque `Handle`, page allocator, no libc). - The new `zig-ffi-ci.yml` runs `zig fmt --check`, `zig build test` (45 tests) and the `hyperpolymath/cicd-suite` purity check. - The only `std.io` use, in `tentacles.zig`, is gone, and `poll_events` gained tests. - Scope: "check passing" means the purity grep passes. No Zig adapter library exists to adopt. **4. CI fixes.** - `chapel-ci.yml` builds Zig with `-Dcpu=baseline`. The artifact runs on a different runner, and that caused the SIGILL in "Rust Build with Chapel Feature" on main. - `rust-ci.yml` check, clippy and test now pass `--workspace`. Before, only the root package was tested, so the `echidna-core` and trust-kernel tests never ran. **5. Idris2 ABI.** - Added `%default total` to `EchidnaABI.Gnn` and `EchidnaABI.TacticRecord`; the package still type-checks. - Planted-positive control: a non-terminating function is rejected. - `CapnSchemas.idr` and `NeSyAssistTesting.idr` are not in the ipkg, so CI does not check them. This is recorded in the wiki table. **6. Creusot: precisely why it is not in CI.** - `cargo check -p echidna-core-creusot --features creusot` fails with 34 errors, because `creusot-contracts` is not a dependency. - The nightly pin is stale, and the documented install path is wrong for current Creusot. - `CREUSOT-SETUP.adoc` no longer claims the job is a hard gate or that milestones 8c-M1..M3 are done. The annotations remain **stated, not proved**. ## Verification (local, rustc 1.99.0) - `cargo fmt --all -- --check` passes. - `cargo clippy --locked --workspace --all-targets -- -D warnings` passes. - `cargo test --locked --workspace --all-targets` passes. - `zig build test` passes: 45/45 on Zig 0.15.2. - `idris2 --build src/abi/echidnaabi.ipkg` passes on Idris2 0.7.0. - `gh actions-lock --no-fix` is clean over 35 workflows. ## Not in this PR - absolute-zero as a cross-prover test corpus (ADOPT-NOW in the types fit map). It needs prover binaries in the live matrix and a pinned corpus manifest, which is out of this increment. - UUID minting is unchanged. It is already centralised in `src/rust/ids.rs`, and this PR mints no IDs. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
First-run start point for echidna: CI restored, descriptor drift fixed, reproducibility pinned, ids centralised, community health and wiki source brought to the rsr-template form.
Commits
startup_failuresince 2026-07 because the local reusable workflow used tag refs undersha_pinning_required..hypatia-baseline.jsonfrom 352 to 56 entries that still match (Re-arm the hypatia baseline gate: generate .hypatia-baseline.json (152 findings to grandfather + burn down) #314).echidna::ids.new_record_id()returns UUIDv7.content_id()returns UUIDv8: SHA-256 over the JCS bytes, per RFC 9562 B.2.temp_token()is for temp-file names. The ADR is indocs/decisions/2026-10-05-id-minting.adoc.Status of each part (§6 terms)
cargo fmt --check,cargo clippy --workspace --all-targets -D warningsandcargo test --workspace --locked(lib, integration and doctests) pass locally on 1.99.0. Two doctests that had never compiled are fixed.gh actions-lock --no-fixis clean across 35 workflows.echidna-core-creusot, renamed from-spark, has annotations that are stated, not proved. The verify job runs on manual dispatch only.content_id: implemented and tested. It is not yet wired to goals, corpus or octads..github/rulesets/*.json: payloads only. They are not applied; applying them is an owner action.echidna prove --output json(echidna.prove.result/1) is not in this PR.Deferred red checks (§5c item 3)
Rust Build — Real Chapel Library (allow-fail, L2.3+ gate)is deferred to ci: 'Rust Build — Real Chapel Library' fails to link (undefined chapel_* symbols) #408. It is a pre-existing link failure (undefinedchapel_*symbols) and is also red onmain.Later commits on this PR
rust-ci.ymlis now a plain workflow. The local reusable still ended in a zero-job "workflow file issue". The job names keep the canonicalrust-ci / …contexts.6a2/→descriptiles/,-spark→-creusot).Left alone
_chora.deedmigration waits for the estate-wide rename.🤖 Generated with Claude Code