Agentic fix to universe checking by elefthei · Pull Request #42 · vellvm/ctrees

elefthei · 2026-10-12T17:17:47Z

Hey folks! I hope all is well since we last talked. I was evaluating the performance of LLMs on hard proof engineering tasks and I decided to try resolving the "Unset Universe Check" issue which has been
with ctrees for several years. This PR removes the universe-checking workarounds by fixing the underlying constraints, particularly where event and branch response universes were tied to tree carriers.

It also updates the build for Rocq/Dune and repairs the affected interpreters and example proofs, restoring the usual trigger and bind equations. Existing declarations and notation are preserved; no new
axioms or admitted proofs were added.

I checked the full build on Rocq 9.3.0, feel free to review and comment.

Copilot

🟡 Changes recommended

The legacy Docker CI still targets Coq 8.15 and cannot validate the newly required Rocq/Dune toolchain.

1 open finding

Update Docker CI to test supported Rocq and Dune versions · New

What changed in this PR

Makes choice trees universe-polymorphic, removes disabled universe checking, updates affected proofs, and migrates builds to Rocq/Dune syntax.

Changes:

Separates event, branch, result, and tree-carrier universes.
Repairs interpreter, recursion, equivalence, and example proofs.
Migrates Dune stanzas to Rocq.

File	Description
`README.md`	Documents enabled universe checking.
`dune-project`	Requires Dune 3.24 and Rocq 0.11.
`theories/dune`	Migrates the main theory to Rocq.
`theories/Core/CTreeDefinitions.v`	Makes core trees and atomic operations universe-polymorphic.
`theories/Core/Index.v`	Enables universe polymorphism.
`theories/Core/Utils.v`	Generalizes trigger and branch classes.
`theories/Eq/Epsilon.v`	Enables universe polymorphism.
`theories/Eq/Equ.v`	Adds polymorphic atomic equations and repairs proofs.
`theories/Eq/IterFacts.v`	Enables universe polymorphism.
`theories/Eq/SBisim.v`	Repairs strong bisimulation proofs.
`theories/Eq/SBisimAlt.v`	Enables universe polymorphism.
`theories/Eq/SSim.v`	Repairs simulation proofs.
`theories/Eq/SSimAlt.v`	Repairs alternate simulation proofs.
`theories/Eq/Shallow.v`	Enables universe polymorphism.
`theories/Eq/Trace.v`	Adds rewriting support for trace heads.
`theories/Eq/Trans.v`	Separates transition-label universes and updates proofs.
`theories/Eq/Visible.v`	Enables universe polymorphism.
`theories/Eq/WBisim.v`	Updates converse notation for Rocq compatibility.
`theories/Interp/Fold.v`	Generalizes fold and interpreter signatures.
`theories/Interp/FoldCTree.v`	Makes tree interpreters universe-polymorphic.
`theories/Interp/FoldStateT.v`	Generalizes state interpreters and repairs equations.
`theories/Interp/ITree.v`	Generalizes interaction-tree embedding.
`theories/Interp/Internalize.v`	Separates source and destination universes.
`theories/Interp/Recursion.v`	Generalizes recursive interpreters and calls.
`theories/Interp/RecursionFacts.v`	Updates recursion equivalence proofs.
`theories/Interp/Refine.v`	Repairs refinement proofs under universe checking.
`theories/Misc/Head.v`	Generalizes head actions.
`theories/Misc/Pure.v`	Makes purity predicates polymorphic.
`examples/AltBisim/dune`	Migrates the example theory to Rocq.
`examples/CCS/Denotation.v`	Generalizes CCS trees and repairs transition proofs.
`examples/CCS/OpDenot.v`	Removes disabled universe checking.
`examples/CCS/dune`	Migrates the CCS theory to Rocq.
`examples/Coffee/coffeeCTree.v`	Updates transition-based example proofs.
`examples/Coffee/dune`	Migrates the Coffee theory to Rocq.
`examples/ImpBr/ImpBr.v`	Generalizes computation universes and notation.
`examples/ImpBr/dune`	Migrates the ImpBr theory to Rocq.
`examples/SimpleSim/SimExample.v`	Updates trigger equation rewrites.
`examples/SimpleSim/dune`	Migrates the simulation theory to Rocq.
`examples/Yield/Lang.v`	Generalizes semantic interpreters and proofs.
`examples/Yield/Par.v`	Separates scheduler tree universes.
`examples/Yield/Util.v`	Generalizes vector-tree utilities.
`examples/Yield/dune`	Migrates Yield and adds Equations.
`tests/ImpBrTest/ImpBrEx/ImpBrEx.v`	Removes disabled universe checking.
`tests/ImpBrTest/ImpBrEx/dune`	Migrates the test theory to Rocq.
`tests/ImpBrTest/extracted/Extract.v`	Removes disabled universe checking.
`tests/ImpBrTest/extracted/dune`	Migrates extraction to Rocq.

🧠 Review effort: Balanced

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

YaZko · 2026-10-13T04:58:34Z

Hey Lef, hope you are doing great on your side!

That's interesting, I had luck with Claude diagnosing a similar issue in a development, trying at some point for ctrees was in the back of my mind. Thanks for giving it a shot!!

In the other library I tried it I was quite happy to get the problem boiled down to a single specific definition for which an alternate definition relaxed constraints.

Here things are a lot more complex visibly. From a quick glance:

It made all definitions in the library universe polymorphic
But it also hardwired a lot of universes explicitly by hand (or whatever appendage these LLMs have)
Annoyingly, it rewrote some proofs, notably proofs using relationalAlgebra. I wonder if it's a related necessity.
But also some seemingly random proofs, like it seems to avoid using intuition. Is it also for the universes, or is it random?
It avoided importing interpFacts which is not too surprising as it is close to have some universe issues there as well.
And a whole bunch of random things (unfolding in some places the ~> notation, ...) that I don't know if they are related to the universe issue or not.

That's both satisfying and frustrating! Did it produce some kind of summary explanation by any chance to get a better sense of what is going on?

Thanks again!

YaZko · 2026-10-13T05:05:43Z

 Section ctree.

-  Context {E : Type -> Type} {B : Type -> Type} {R : Type}.
+  Universe e b.


Need to understand if and why this manual pinning of the universes is necessary.

The names tie VisF/BrF response types to the E/B domains without tying those domains together.

YaZko · 2026-10-13T05:07:19Z

+  End CTree.
+
+  Section AtomicTrees.
+    Universes d q.


It's even more mystifying to me in this section. It doesn't seem to explicitly tie any specific universes together, why not let universe polymorphism run its course?

These preserve independently instantiable constructor carriers; the regression checks strictly larger carriers (i < ri < qi) and bind across different carrier universes.

YaZko · 2026-10-13T05:08:12Z


-#[global] Instance MonadTrigger_ctree {E F B} `{E -< F} : MonadTrigger E (ctree F B) :=
-  fun _ e => trigger e.
+#[global] Instance MonadTrigger_ctree@{d q +} {E : Type -> Type} {F : Type -> Type} {B}


Need to check what is this + notation. Is it just to name the two first universes but let the others be handled normally? Unsure.

Yes: + lets Rocq infer the remaining universes, while d and q name the carrier levels rather than fixing concrete universe values.

YaZko · 2026-10-13T05:09:58Z


-Polymorphic Class MonadTrigger (E : Type -> Type) (M : Type -> Type) : Type :=
-  mtrigger : forall {X}, E X -> M X.
+Polymorphic Class MonadTrigger@{ei +}


Ah here I maybe (emphasis on maybe) understand better: the input of E and the type on which we quantify can indeed be enforced to be equal, that sounds reasonable.

Exactly: mtrigger quantifies over the same response universe as E’s domain, and mbr does the analogous thing for branches.

YaZko · 2026-10-13T05:10:49Z

    rewrite <- x in EQu.
    dependent destruction EQu.
-    rewrite <- x. eauto.
+    rewrite <- x.


But surely we don't have to carefully not call eauto in some contexts just to please the universes? That would simply not be sustainable.

Agreed; I restored the original eauto proof, which compiles with universe checking enabled.

YaZko · 2026-10-13T05:11:08Z

 Proof.
  intros R t u EQ; inv EQ.
-  apply Equ_clos with u' t'; intuition.
+  apply Equ_clos with u' t'; intuition; symmetry; assumption.


It really seems to hate intuition. Why?

There was no need to avoid it here; I restored the original intuition proof and checked it with universe checking enabled.

YaZko · 2026-10-13T05:13:07Z

+  (CTree.trigger e : @ctree@{_ _ _ _ d q} E B X) = Vis e (fun x => Ret x).
+Proof. reflexivity. Qed.
+
+Lemma bind_trigger {X Y}


It also seems to avoid using the monad type class. That makes sense as it probably tried to find a repo-local solution when fundamentally it's a cross repo one.

The Monad instance remains; this lemma exposes different input/output tree universes, whereas ExtLib’s bind uses a single M.

Keep required universe boundaries, restore existing proof structure, and retain only necessary polymorphism. Remove the unused trace instance and use native converse notation in WBisim. Validated on Rocq 9.3.0 with OCaml 5.4.1 and Dune 3.24.2: full build, UniverseCheck, kernel recheck, focused source probes, and ImpBr consumer. Rocq 9.0 and 9.2 CI remain required.

Align Nix with the passing Docker toolchain and pin coinduction v1.22 and relation-algebra v1.9.1. Update the declared compiler minimum and README to Rocq 9.2. The former Rocq 9.0 dependency combination fails a universe-checked RelationAlgebra/ITree facts import without loading any CTree code. The repaired dependency import and exact Nix package build pass locally; the Rocq 9.3 build, UniverseCheck, and ImpBr consumer also pass.

Copilot

🟡 Changes recommended

The dependency bounds permit RelationAlgebra versions that cannot parse the new converse notation.

1 open issue

Require RelationAlgebra 1.9.0 for the new notation · New

1 resolved since last review

Update Docker CI to test supported Rocq and Dune versions

_{Review effort: Balanced}

elefthei · 2026-10-17T01:01:28Z

Hey Yannick, thanks for the careful review! You were right that the first pass mixed the universe fix with a lot of unnecessary churn. I’ve pushed 1b688f3, reverting those proof rewrites—including the eauto, intuition, and relational-algebra changes—restoring InterpFacts and ~> notation, and removing redundant polymorphism settings.

The remaining annotations keep event/branch response domains and tree-carrier universes separate, including across bind and interpretation. I also added a regression with strict universe inequalities to check that these boundaries really stay independent, rather than just making the examples compile.

The full build, kernel recheck, and ImpBr example pass locally on Rocq 9.3 and should pass on the CI as well. I bumped the versions of Rocq and dune, might as well.

Agentic fix to universe checking

a0b0a2f

elefthei requested review from YaZko and nchappe and a balanced review from Copilot October 12, 2026 17:17

Copilot started reviewing on behalf of elefthei October 12, 2026 17:18

View session

Copilot AI reviewed Oct 12, 2026

View reviewed changes

Comment thread dune-project

elefthei added 2 commits October 12, 2026 13:05

Fix CI toolchains and cross-version proof compatibility

6f1c3d3

Fix Docker CI checkout ownership

7bb7681

YaZko reviewed Oct 13, 2026

View reviewed changes

elefthei added 2 commits October 16, 2026 15:41

elefthei requested a balanced review from Copilot October 17, 2026 00:29

Copilot started reviewing on behalf of elefthei October 17, 2026 00:30

View session

Copilot AI reviewed Oct 17, 2026

View reviewed changes

Comment thread theories/Eq/WBisim.v

Require RelationAlgebra 1.9.0 for converse notation

748a488

elefthei requested a review from YaZko October 17, 2026 20:09

Conversation

elefthei commented Oct 12, 2026

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Uh oh!

Uh oh!

YaZko commented Oct 13, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

🟡 Changes recommended

Uh oh!

Uh oh!

elefthei commented Oct 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

elefthei commented Oct 17, 2026 •

edited

Loading