Skip to content

Commit 4920e04

Browse files
chore: unblock CI — revert 5 dependabot major bumps + .trusted-base-ignore FP fix + deno.lock populate (#128)
## Summary — auto-merge deadlock breaker This branch bundles **three** required-check fixes that had been split across PRs #126, #127, #128 — but each PR's required-checks failed because they depended on the others. Solo PRs deadlocked; this PR closes the chain. ### Bundled commits 1. **`chore(deps): revert 5 dependabot major-version bumps that broke CI`** (original #128 scope) Five dependabot major bumps merged 2026-05-29 without call-site updates: axum 0.7→0.8 (#120), rand 0.9→0.10 (#121), criterion 0.5→0.8 (#122), nom 7→8 (#123), rustyline 15→18 (#124). Each shipped real API breaks: - rand 0.10 renamed `Rng` → `RngExt` (because upstream `rand_core` renamed `RngCore` → `Rng`); `use rand::Rng` no longer brings `random_range` / `random` in scope. - nom 8 moved from closure-based to trait-based combinators (`alt(args)(input)` → `alt(args).parse(input)`). - axum 0.8 transitively pulls a different tower-http (compile mismatch in `follow_redirect/policy/mod.rs`). Reverts all 5 back to the May-28 working state. `cargo check --lib` cleans in ~2 min locally. 2. **`chore(governance): populate empty deno.lock with minimal valid v4 lockfile`** (was #127) Replaces the 0-byte `deno.lock` (tracked since 3b03087 for sweep visibility) with `{"version":"4","remote":{}}`. Unblocks `governance / Language / package anti-pattern policy` which fails on `deno run` lockfile parse before reaching the actual `.ts` walk. 3. **`chore(governance): clear 12 trusted-base false-positive escape hatches`** (was #126) Adds `.trusted-base-ignore` for 4 Rust pattern-detector tables (10 hits) — same FP class as the believe_me audit in `docs/PROOF-NEEDS.md` (zero real escapes). Adds `-- AXIOM:` / `-- TRUSTED:` magic-word lines in the script's 5-line window for two real Agda postulates (`funext`, `Conflicts`). ## Why bundled Each individual PR failed its OWN required checks because it depended on the others' fixes: - #128 (revert) needed `governance / Language / package anti-pattern policy` → fixed in #127 - #128 (revert) needed `governance / Trusted-base reduction policy` → fixed in #126 - #126 + #127 needed `T1 / *` live-provers GREEN → fixed in #128 Bundling resolves the chicken-and-egg. #126 and #127 are closed as superseded with backlinks. ## Verification - Local: `cargo check --lib` clean (1m 52s). - PR #126 had `Trusted-base reduction policy: SUCCESS` and `Validate K9 / A2ML / eclexiaiser: SUCCESS` before being closed — proves the fix works in isolation. - PR #127 had `Language / package anti-pattern policy: SUCCESS` before being closed. - All three classes of CI failure are now addressed in this single PR. ## Seam-gaps captured (out of scope) 1. **Dependabot major bumps + always-auto-merge interact badly**. Per the standing estate hook `feedback_always_automerge_prs`, auto-merge is universal. For major bumps without paired code updates, that's structurally unsafe — the only checks that DID gate the merges (validation gates) don't compile the workspace. Worth a follow-up: either Dependabot config to draft major bumps, or a per-repo guard requiring manual review for major-version-only PRs. 2. **`standards check-ts-allowlist.ts` could pass `--no-lock`** — the script is a read-only file walker that doesn't import anything, so the lockfile is irrelevant. Adding `--no-lock` makes it robust to this entire failure class estate-wide. 3. **`standards rust-ci-reusable` doesn't pass `--locked`** — `cargo check` / `cargo test` happily auto-update Cargo.lock during CI, masking version drift. Adding `--locked` to the reusable would surface drift the first time it happens, instead of when the next major hits. ## Test plan - [x] Local `cargo check --lib` clean. - [ ] CI: all required checks GREEN on this branch. - [ ] `T1 / z3`, `T1 / vampire`, `T1 / spass` GREEN (already verified GREEN on the first push of #128). Refs: #92 (broader baseline failures — this PR addresses the compile + trusted-base + language-policy slices). Supersedes #126, #127.
1 parent e1c025f commit 4920e04

6 files changed

Lines changed: 401 additions & 312 deletions

File tree

.trusted-base-ignore

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
# .trusted-base-ignore — whole-path exemptions for the trusted-base scanner
2+
# (hyperpolymath/standards check-trusted-base.sh).
3+
#
4+
# Format: each non-comment, non-blank line is a path-fragment substring that
5+
# exempts every marker whose file path contains the fragment.
6+
#
7+
# Use sparingly. Per-site `TRUSTED:`/`AXIOM:` comments remain the preferred
8+
# mechanism for one-off documented escapes; this file is for whole-path
9+
# exemptions where the file's *entire purpose* is to talk about the patterns
10+
# the scanner detects (so every occurrence is a string literal, not a use).
11+
12+
# ─────────────────────────────────────────────────────────────────────────────
13+
# Pattern-detector tables (NOT uses of the patterns themselves)
14+
# ─────────────────────────────────────────────────────────────────────────────
15+
# Each of the files below holds a `Vec<DangerousPattern>` (or equivalent)
16+
# that enumerates the very `unsafePerformIO`/`unsafeCoerce`/`believe_me`
17+
# string literals the scanner is hunting for. The scanner's naive
18+
# substring grep cannot distinguish "uses the pattern" from "names the
19+
# pattern in a detector table", so every entry shows up as a false
20+
# positive. Same FP class as the `\bbelieve_me\b` Idris2 audit recorded
21+
# in docs/PROOF-NEEDS.md §"believe_me audit (2026-05-18)".
22+
#
23+
# These files are the *implementation* of the trust-pipeline's
24+
# axiom-tracker — they're proof infrastructure, not proof escapes.
25+
src/rust/verification/axiom_tracker.rs
26+
crates/echidna-core-spark/src/axiom_tracker.rs
27+
28+
# ─────────────────────────────────────────────────────────────────────────────
29+
# Hazard-classification helpers in the corpus extractor (NOT uses)
30+
# ─────────────────────────────────────────────────────────────────────────────
31+
# `corpus/agda.rs::collect_hazards` and `corpus/idris2.rs::collect_hazards`
32+
# each run a single-line `if text.contains("unsafePerformIO" / "unsafeCoerce"
33+
# / "Obj.magic")` to flag corpus entries that *contain* those patterns.
34+
# Same FP class — the substring is a hazard sentinel, not an escape hatch.
35+
src/rust/corpus/agda.rs
36+
src/rust/corpus/idris2.rs

0 commit comments

Comments
 (0)