Repository navigation
docs(proofs): inventory Agda-first reconciliation without retiring Idris2 - #137
Conversation
Codex Review SummaryThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
No actionable comments were generated in the recent review.
 |
| Layer / File(s) | Summary |
|---|---|
Reconciliation inventory verification/proofs/AGDA-RECONCILIATION.adoc |
The document lists candidate theory areas and their Agda and Lean/Coq statuses. It specifies an Agda check followed by separate Coq/Rocq and Lean inspection for implementation-independent claims. Reconciliation requires statement correspondence, with versions, revisions, assumptions and a correspondence receipt recorded in the owning proof status. |
Estimated code review effort: 1 (Trivial) | ~5 minutes
Change: Other
Possibly related PRs
- hyperpolymath/vcl-ut#126: Updates the Idris2 proof-corpus gate and wire proof modules that the reconciliation inventory identifies as existing engineering checks and obligations.
- hyperpolymath/vcl-ut#128: Adds Idris wire-conformance proofs and decoder tests for wire obligations listed in the inventory.
Merge Risk: 
4a2ca
-
The inventory makes no completed proof-port claims and preserves the existing engineering checks. No actionable merge-blocking risk is identified.
Pre-merge checks: 
-
Check name Status Explanation Resolution Description check The description accurately summarises the document and its scope, but it does not follow the required template. It omits the Summary, Changes, RSR Quality Checklist, Testing, and Screenshots sections. Add the required template sections. List the key changes, complete the RSR Quality Checklist, and describe the testing performed. State that Screenshots are not applicable if no screenshots or terminal output exist. -
Check name Status Explanation Title check The title clearly identifies the Agda reconciliation inventory and states that Idris2 remains in place. It accurately summarises the main change. Docstring Coverage No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentat… Linked Issues check Check skipped because no linked issues were found for this pull request. Out of Scope Changes check Check skipped because no linked issues were found for this pull request. Full details: Docstring Coverage
-
Explanation
No eligible functions found in the changed files. Skipping docstring coverage check. Docstring coverage is scoped to functions touched by this diff with cyclomatic complexity of at least 2. Documentation-only edits and deletions within surviving functions are included; unchanged diff context and fully deleted functions are excluded. Analyzed 0 functions across 0 files. (1 skipped: 1 unsupported.)
-
-
- Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts
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.
|
![coderabbitai[bot]](https://avatars.githubusercontent.com/in/347564?s=60&v=4){kind=small}
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4a2ca0f2d1
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| |=== | ||
| |ID |Source and intended theory statement |Agda |Lean/Coq + bridge | ||
| |VCL-L4 |The proof of `NoRawUserInput` preservation under the specified statement join in `src/core/Composition.idr`; inspect actual definition of `joinWhere` and literal recognition rather than replacing it with a toy Boolean |OPEN |OPEN — exact proposition and source/target correspondence not yet compared | ||
| |VCL-L6–L10 |Composition closure for the actual indexed level predicates in `Composition.idr` |OPEN |OPEN — do not presume universal level monotonicity |
There was a problem hiding this comment.
When this ledger guides the Agda port, describing all of L6–L10 as composition closure asks for a false unconditional L10 theorem: src/core/Composition.idr:820-839 explicitly shows that two individually acyclic L10 requirement sets can become cyclic when joined, so l10Compose requires epiNoCycle (composeJoin q1 q2) = True. Split L6–L9 from L10 or record this JoinSideCondition, otherwise the instruction below to reprove the “exact theorem” misstates the actual obligation.
Useful? React with 👍 / 👎.
|
|
||
| [source,shell] | ||
| ---- | ||
| agda --safe --without-K --cubical-compatible <module.agda> |
There was a problem hiding this comment.
When a reader copies this [source,shell] recipe, <module.agda> is parsed by Bash and other POSIX shells as input/output redirection, and the trailing > has no target, so the shell exits with a syntax error before Agda runs. Use an ordinary example path such as path/to/Module.agda or a quoted variable instead.
Useful? React with 👍 / 👎.
|
|
||
| [cols="1,3,2,3",options="header"] | ||
| |=== | ||
| |ID |Source and intended theory statement |Agda |Lean/Coq + bridge |
There was a problem hiding this comment.
When an obligation has been reconciled in only Lean or only Coq/Rocq, this combined status cell cannot represent which prover remains open or attach the per-prover version and correspondence receipt required below. Because line 37 explicitly requires the two inspections separately, split this into independent Lean and Coq/Rocq columns or records so completing one cannot be mistaken for completing both.
Useful? React with 👍 / 👎.
Adds
verification/proofs/AGDA-RECONCILIATION.adoc: concrete L4, L6–L10, epistemic/transition and engineering/wire obligations with statuses OPEN, canonical Agda command, three-prover bridge requirements and explicit independence from Mathesis/ECHIDNA. Preserves the existing source-grounded Idris2 corpus, honesty guard and CI unchanged. No Agda port or external witness is claimed.