feat(hydro_lang): capture fold commutativity/idempotency in IR nodes

[jhellerstein]

Adds IsProved trait to the properties module and records algebraic properties directly on fold/reduce IR nodes, enabling downstream analysis passes to distinguish lattice operations from non-commutative/non-idempotent ones without re-deriving properties from types.

Changes:

• properties/mod.rs: IsProved trait with const IS_PROVED: bool
• compile/ir/mod.rs: is_commutative/is_idempotent fields on Fold, FoldKeyed, Reduce, ReduceKeyed, ReduceKeyedWatermark
• stream/mod.rs, keyed_stream/mod.rs: IsProved bounds on fold/reduce, capture proof status at construction
• viz/render.rs: pattern matches updated with ..
• Snapshot updates for IR tests in hydro_test and compile-fail stderr

Cherry-picked from the coord-criterion branch.

[Copilot]

Pull request overview

This PR enhances hydro_lang’s IR so downstream compiler/analysis passes can directly determine whether a fold/fold_keyed accumulator was proven commutative and/or idempotent, without re-deriving those facts from types/proof annotations.

Changes:

• Add an IsProved trait (with const IS_PROVED: bool) for proof marker types (Proved vs NotProved).
• Extend HydroNode::Fold and HydroNode::FoldKeyed with is_commutative / is_idempotent boolean fields.
• Capture and store proof status at fold construction sites in Stream::fold and KeyedStream::fold.

Reviewed changes

Copilot reviewed 4 out of 4 changed files in this pull request and generated no comments.

File	Description
hydro_lang/src/properties/mod.rs	Introduces IsProved to reflect proof-marker status as a compile-time boolean.
hydro_lang/src/live_collections/stream/mod.rs	Records commutativity/idempotence proof status onto HydroNode::Fold at construction.
hydro_lang/src/live_collections/keyed_stream/mod.rs	Records commutativity/idempotence proof status onto HydroNode::FoldKeyed at construction.
hydro_lang/src/compile/ir/mod.rs	Adds is_commutative/is_idempotent fields to Fold IR nodes and preserves them through deep_clone.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[Copilot]

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 1 comment.

[cloudflare-workers-and-pages]

Deploying hydro with    Cloudflare Pages

Latest commit:	fb5d5ae
Status:	✅  Deploy successful!
Preview URL:	https://7e9258cb.hydroflow.pages.dev
Branch Preview URL:	https://feat-is-proved-fold-properti.hydroflow.pages.dev

View logs

[Copilot]

Pull request overview

Copilot reviewed 4 out of 4 changed files in this pull request and generated 2 comments.

[Copilot]

Pull request overview

Copilot reviewed 5 out of 5 changed files in this pull request and generated 2 comments.

[shadaj]

Hmm, so @Benjscho recently changed the IR generation so that for commutative (and maybe idempotent, I don't remember?) folds we no longer generate an ObserveNonDet and instead directly emit the IR node on the unordered stream. So I think you could just look at the input collection metadata to identify whether it is a proven commutative fold or not.

The broader principle is that there are never unproven properties in the IR, either it's proven (perhaps weakly through manual_proof) or the operator wouldn't compile. Note that in the future, we might want to tag the strength of the proof, but lack of a proof shouldn't be one of the options so want to avoid polluting the IR with duplicate metadata.

[jhellerstein]

@shadaj the nomenclature is certainly not helpful. All it's supposed to be doing is memoizing that the node was found to be commutative and/or idempotent. But your point I think is this:

• If the input to a fold in the IR is NoOrder, the fold was found to be commutative
• If the input to a fold in the IR is AtLeastOnce, the fold was found to be idempotent
  So the memoization is trivial.

Am I getting that right?

[shadaj]

Yes exactly! We try to avoid memoization directly within the IR if possible because it's easy to accidentally have rewrites that leave the IR inconsistent.

[jhellerstein]

Closing — as discussed with @shadaj, commutativity/idempotency can be inferred from the fold's input collection_kind (NoOrder → commutative, AtLeastOnce → idempotent). No need to memoize in the IR. PR #2927 will be updated to infer directly.