fix: real SHA-pinning check, real Justfile targets, and docs that match the code

[hyperpolymath]

Three independent commits, each droppable on its own. Two fix gates that could never fail; one fixes documentation that actively misdirects.

---

1. docs: — two files misstate the code they describe

PROOF-NEEDS.md

Claimed "1 Admitted in proofs/coq/lambda/LambdaCNO.v (y_not_cno)". Measured against absolute-zero @87902bb7:

$ grep -rn "Admitted" absolute-zero --include=*.v | wc -l
0
$ grep -rn "^Axiom"  absolute-zero --include=*.v | wc -l
23

Zero Admitted. Twenty-three Axioms across 6 files. The old wording was wrong in both directions — it overstated the incompleteness and understated the trusted base 23×.

Why this matters operationally: an Axiom passes a "no sorry / no Admitted" gate silently. Counting only Admitted measures the wrong thing.

y_not_cno is a KEPT AXIOM with a written rationale (LambdaCNO.v:388-399), not an unproven hole — and it is not the "concrete, closable proof obligation" the old text claimed. The in-source note explains it needs an invariant closed under the full reduction congruence, or a coinductive/step-indexed argument.

The doc now defers to the AXIOM AUDIT already in physics/LandauerDerivation.v, which is notably self-critical — it records that cno_zero_energy_dissipation_derived is an axiom despite its _derived name, and that the triage docs' "DISCHARGE" marks are inaccurate.

Promoted to the top of "What Needs Proving" — the audit's own SOUNDNESS WARNINGS: prob_nonneg and prob_normalized are false over unconstrained function-type distributions, and shannon_entropy_maximum's inequality is backwards (asserts uniform minimises entropy). All three are currently unused — cheap now, expensive later.

aletheia/CLAUDE.md

Said "all core logic lives in src/main.rs (~950 lines)" and "don't split into modules unless >1000 lines". It has been 5 modules / 995 lines for a while, main.rs at 121. That instruction would tell the next agent to undo the existing structure.

Also corrected: 23 workflows → 16; flake.nix listed but absent; 18 integration tests → 32. Added a prominent warning that those 16 nested workflows have never run (root-only discovery) — the fault that let this crate stay uncompilable for a month.

---

2. fix(aletheia): — the SHA-pinning check could never fail

if line.contains("@v") && !line.contains("@") {

contains("@v") implies contains("@"), so the second clause is always false and has_unpinned could never be set. Proven before changing anything:

uses: actions/checkout@v4    old_detects_unpinned=false

This is aletheia's Silver-level "GitHub Actions SHA pinning" check — and pointedly, the exact check that would have caught SonarSource/sonarqube-scan-action@master, the unpinned action that broke this repo's Governance and CodeQL in #139.

Replaced with uses_line_is_pinned, requiring 40 hex chars after the final @, which also:

• accepts the inline - uses: form (the estate's existing linter anchors to line-start and misses it)
• ignores a trailing # v7.0.1 provenance comment, so a correct pin with a stale comment isn't a false positive
• exempts ./… local actions/reusables and docker:// refs

Also replaced assert!(true) in test_file_exists with a real assertion, anchored on env!("CARGO_MANIFEST_DIR") so it is deterministic regardless of CWD.

Verified: 29 unit tests (was 26) · cargo fmt --check clean · clippy 25 → 23. End-to-end cargo run -- . now reports [FAIL] GitHub Actions SHA pinning, correctly finding the one genuinely unpinned action — where before the fix it reported a pass.

Refs #125.

---

3. fix(#99): — root Justfile was a fake gate

build:
    @echo "Build not configured yet"

build, test, fmt, lint, clean all printed a string and exited 0. Wired to the same commands root rust-ci.yml runs, in the same order, so just check means what CI means.

Two deliberate limits, documented in the recipes so nobody "fixes" them:

• test is --bins only — the integration suite is a spec for a CLI that doesn't exist; 27/29 fail by design (aletheia: 27/29 integration tests fail — main.rs never wires up the CLI surface #124). Adding --tests would make the bar green by breaking it.
• lint is not yet -D warnings (aletheia: clippy -D warnings has 25 findings — add as blocking gate once clean #125). When that closes it must be added here and to rust-ci.yml together, so local and CI never disagree.

Verified by running them, not reading them: just deps-check → OK: zero dependencies; just test → 29 passed; just check → exit 0.

And verified the gate can actually fail — appending badly-formatted Rust makes just fmt exit 1 while just build still exits 0; reverting restores 0. A gate nobody has watched fail is not a gate.

Closes #99.

---

Not in this PR

• aletheia: 27/29 integration tests fail — main.rs never wires up the CLI surface #124 — still blocked on the source-of-truth question for RSR checks
• guix.scm identity/licence clobber — separate, more urgent: fix: restore guix.scm identity and licence (squisher-corpus clobber is live on main) #143

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 1 resolved / 1 findings

Fixes GitHub Actions SHA-pinning validation, wires the root Justfile targets to real cargo commands, and corrects inaccurate documentation. Consider handling dynamic action references in the SHA-pinning check to prevent false positives on expression-driven uses lines.

Auto-approved and auto-merge armed: No blocking issues found.
Please see Auto-approve Docs for details on setting custom approval criteria. — merges when pipeline and required approvals pass.

✅ 1 resolved

✅ Edge Case: Dynamic action refs flagged as unpinned

📄 aletheia/src/checks.rs:207-210
A uses: value driven by an expression such as uses: ${{ matrix.action }}@${{ matrix.sha }} or uses: ${{ inputs.action }} has no literal 40-hex SHA after the final @, so uses_line_is_pinned returns false and the whole workflow is marked non-pinned — a false positive for repos that pin via a matrix/variable. This is a rare edge case and only affects reporting, but if such patterns are used you may want to exempt values containing ${{.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}

[gitar-bot]

⚠️ Gitar auto-approved this PR but could not enable auto-merge: auto-merge is disabled for this repository — enable "Allow auto-merge" in the repository settings.

[gitar-bot]

Gitar has auto-approved this PR and enabled auto-merge (configure)