feat: Idris2-only proofs, e2e CI, emitter, backend/projection specs

[hyperpolymath]

Why

Finish the outstanding list after #69: Idris2-only FV, SHA-pinned e2e jobs, fail-closed manifest emitter, backend + projection specs, G1.1 conversion of live 6a2/bot/policy deeds.

Not closing

Do not close #5–#10. No Core checker, no accepted evidence, no accepting projection, no preserving lowering, ABI-1 typecheck SKIP without idris2.

Housekeeping

Rotate the PAT used this session.

[coderabbitai]

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

Configuration used: Organization UI

Review profile: ASSERTIVE

Plan: Advanced

Run ID: 1249395e-9603-4f4c-a507-c31b07f120b0

📥 Commits

Reviewing files that changed from the base of the PR and between 8abde15 and 861c6c2.

⛔ Files ignored due to path filters (1)

• .github/workflows/actions.lock is excluded by !**/*.lock

📒 Files selected for processing (37)

• .github/workflows/e2e.yml
• .machine_readable/6a2/AGENTIC.deed
• .machine_readable/6a2/LANGUAGES.deed
• .machine_readable/6a2/NEUROSYM.deed
• .machine_readable/6a2/PLAYBOOK.deed
• .machine_readable/6a2/STATE.deed
• .machine_readable/6a2/anchors/ANCHOR.deed
• .machine_readable/bot_directives/coverage.deed
• .machine_readable/bot_directives/debt.deed
• .machine_readable/bot_directives/methodology.deed
• .machine_readable/policies/MAINTENANCE-AXES.deed
• .machine_readable/policies/MAINTENANCE-CHECKLIST.deed
• .machine_readable/policies/SOFTWARE-DEVELOPMENT-APPROACH.deed
• Justfile
• build/just/proofs.just
• docs/reports/LANGUAGE-AUDIT.adoc
• docs/status/PROOF-NEEDS.adoc
• docs/status/PROOF-STATUS.adoc
• docs/status/ROADMAP.adoc
• scripts/emit-manifest.sh
• src/backends/BACKEND-CONTRACT.adoc
• src/backends/README.adoc
• src/backends/none/CONTRACT.adoc
• src/backends/zig-ffi/CONTRACT.adoc
• src/manifest/README.adoc
• src/projections/PROJECTION.adoc
• src/projections/README.adoc
• src/projections/null/equivalence-refuse-refuse.witness
• tests/backend_spec.sh
• tests/e2e.sh
• tests/evidence_spec.sh
• tests/projection_spec.sh
• verification/proofs/README.adoc
• verification/proofs/agda/Properties.agda
• verification/proofs/coq/TypeSafety.v
• verification/proofs/lean4/ApiTypes.lean
• verification/proofs/tlaplus/StateMachine.tla

 __________________________________________________________________________________________________
< Estimate to avoid surprises. Estimate before you start. You'll spot potential problems up front. >
 --------------------------------------------------------------------------------------------------
  \
   \   \
        \ /\
        ( )
      .( o ).

✨ Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

---

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.

❤️ Share

• X
• Mastodon
• Reddit
• LinkedIn

_{Comment @coderabbitai help to get the list of available commands.}

[sonarqubecloud]

Quality Gate failed

Failed conditions
C Security Rating on New Code (required ≥ A)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE