Land sweeps + first honest CI: compiler builds, proofs check, fail-closed gates

[hyperpolymath]

What this lands (squash-merge; branch history collapses)

Pre-existing unpushed sweeps (rebased, sitting local-only since July):

• sweep2/3/4 (mise.toml, licence texts + SPDX, C-A-G-M files) and the CodeQL SHA-pin fix.
• The stray LICENSES/AGPL-3.0-or-later.txt from sweep3 is removed (repo policy bans AGPL in three places; same failure class as the phronesis incident). The squashed commit on main never carries it.

Proof repairs — the Idris2 ABI suite had NEVER compiled:

• kitchenspeak.agda-lib: bare -- line rejected by Agda 2.6.4.3's parser, killing every check before it started.
• Idris2: missing import public Data.Nat (exported signatures mention LTE/NonZero/modNatNZ), Idris1-only lteRefl reproven, SIsNonZero misapplied to opaque Nats reformulated as erased premises, erased-field projections moved into 0-quantity proofs with a soUnique proof-irrelevance lemma.
• New kitchenspeak-abi-proofs.ipkg so the suite checks as a whole (per-file --check is the known fake-gate).

Compliance:

• {{REPO}} placeholders filled in META/ECOSYSTEM (unblocks the required openssf-compliance context).
• Root allowlist extended for the sweep's governance/licensing/tooling files — check-root-shape.sh passes locally (49 entries / 51 permitted), so Estate Rules goes green.

New workflow proof-gates.yml — fail-closed by design:

Job	Container	Gates
compiler	debian:trixie	dune build; all examples/v2 positives must type-check; all 10 negatives must be rejected
agda-proofs	debian:trixie	4 proofs (EchoBridge under --safe) against SHA-pinned echo-types/absolute-zero; 6-postulate trusted-base budget
abi-proofs	digest-pinned idris2-pack	--typecheck the ipkg; reject believe_me/assert_total in proof code

Verified locally before push

• dune build clean; 5/5 positive examples pass, 10/10 negatives rejected.
• All four Agda proofs exit 0 (Agda 2.6.4.3, stdlib 2.1, Debian trixie apt).
• Idris2 suite exit 0 on both 0.7.0 (local) and 0.8.0 (the exact digest-pinned image CI uses).
• Trusted-base script, root-shape check, and placeholder check all pass in-tree.

🤖 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 3 resolved / 3 findings

Adds fail-closed CI proof gates alongside OCaml compiler builds and Idris2 ABI suite repairs. Consider tightening the alignment proof edge cases, hardening the escape-hatch grep gate, and cleaning up non-tool entries in mise.toml.

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.

✅ 3 resolved

✅ Edge Case: Alignment proofs are vacuous for zero-alignment fields

📄 verification/proofs/idris2/ABI/Layout.idr:48-54 📄 verification/proofs/idris2/ABI/Compliance.idr:32-42
FieldAligned/sizeAligned were reformulated as (0 nz : NonZero (alignment)) -> modNatNZ ... nz = 0. When fieldAlignment/layoutAlignment is 0, NonZero 0 is uninhabited, so the implication is satisfied vacuously — meaning AllFieldsAligned and CABICompliant provide no guarantee for a malformed (zero-alignment) layout despite their names. This is documented as intentional, but it silently weakens the ABI-compliance theorem. Consider carrying the NonZero witness as a stored premise on the layout/field type (so zero-alignment layouts are unrepresentable) rather than as an antecedent that is trivially dischargeable.

✅ Quality: escape-hatch grep gate is fragile for inline comments

📄 .github/workflows/proof-gates.yml:126-137
The No dangerous escape hatches step excludes only lines whose content starts with the comment marker (:[[:space:]]*--). A trailing/inline comment such as foo = bar -- believe_me does not start with --, so it would trigger a false failure; conversely the gate cannot distinguish a genuine escape hatch used mid-line. Since no such lines exist today the gate passes, but it is brittle. Prefer stripping comments before matching (e.g. sed 's/--.*//' then grep), or match only word-boundary occurrences on code tokens.

✅ Quality: mise.toml lists many entries that are not mise tools

📄 mise.toml:1-15
Several [tools] entries (e.g. denojs, gofmt, vitest, jest, pytest, and the various package managers) are not registered mise short-names/backends, so mise install will likely error out on an unknown tool rather than provisioning them. This makes the toolchain file unusable as-is for anyone running mise install. Verify each identifier against the mise registry (e.g. deno not denojs; test runners generally come via npm/pip rather than a mise tool) and drop or correct the invalid ones.

Options

Display: compact → Showing less information.

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

Compact

gitar display:verbose

---

Important

Your trial ends in 7 days — upgrade now to keep code review, CI analysis, auto-apply, custom automations, and more.

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

[gitar-bot]

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

✅ All code review findings resolved.

_{Configure merge blocking}

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud