Skip to content

Basic Support for Channels - #410

Draft
shankarapailoor wants to merge 2 commits into
mainfrom
shankara/channels
Draft

Basic Support for Channels#410
shankarapailoor wants to merge 2 commits into
mainfrom
shankara/channels

Conversation

@shankarapailoor

@shankarapailoor shankarapailoor commented Apr 15, 2026

Copy link
Copy Markdown
Contributor

Summary

This draft PR adds initial IR support for channels as a new channel dialect in the LLZK dialect family.

Channels model unordered multiset-equality constraints for cross-struct / cross-chip interaction. This PR introduces the IR surface, parser/printer support, and verifier checks needed to represent channel interactions in LLZK. It does not implement backend lowering or the global multiset balance check.

What This PR Adds

  • A new channel dialect with:
    • channel.def
    • channel.push
    • channel.pull
  • Explicit channel payload signatures on channel.def
    • current form: builtin tuple types whose elements are all !felt.type
  • channel.push / channel.pull as symbol-user ops with:
    • variadic tuple operands
    • optional multiplicity operand
    • constraint-only placement via function.allow_constraint
  • Custom parser/printer support for the current textual syntax

Design Notes

  • Channels are implemented as a separate channel dialect, not as ops inside the llzk dialect.
  • channel.def now carries an explicit payload signature instead of inferring schema from use sites.
  • Multiplicity remains a per-use operand on channel.push / channel.pull; it is not part of the channel declaration.
  • The current verifier intentionally accepts a conservative subset of row-local felt expressions:
    • allowed today: felt constants, felt block arguments, struct.readm, array.read, and field-native felt.add / felt.sub / felt.mul / felt.neg
    • rejected today: non-polynomial felt ops, calls, nondet values, and mixed row contexts

Open Questions

  • Should channels take more complex types as input? It might be weird for it to take struct types as input given channels are meant for cross struct interaction.
  • For the verification dialect we might want to specify assumptions and guarantees from the sender and receiver side. @iangneal we may want to consider extending support for the verif dialect to add that. The Clean language has a draft PR proposing something like that: Channels Verified-zkEVM/clean#328 which is definitely useful. We did something similar for Picus engagements where interactions had assumption and post condition annotations depending on whether things were being pushed or pulled.

@github-actions

Copy link
Copy Markdown
Contributor

Test Results

  2 files  ±0    2 suites  ±0   6m 14s ⏱️ +11s
173 tests +2  167 ✅ +2   6 💤 ±0  0 ❌ ±0 
346 runs  +4  334 ✅ +4  12 💤 ±0  0 ❌ ±0 

Results for commit af5a5e1. ± Comparison against base commit 16993e9.

@iangneal
iangneal requested a review from a team April 20, 2026 19:20
Comment on lines +1 to +3
# This is a template that lists the available options when creating a changelog entry file
# Edit according to your changes, before marking a PR as ready for review.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
# This is a template that lists the available options when creating a changelog entry file
# Edit according to your changes, before marking a PR as ready for review.

//
// Part of the LLZK Project, under the Apache License v2.0.
// See LICENSE.txt for license information.
// Copyright 2025 Veridise Inc.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
// Copyright 2025 Veridise Inc.
// Copyright 2026 Project LLZK

Applies throughout, I won't make this comment on every location where this change applies.

The payload signature is declared explicitly on the channel definition. In
this task, the signature is a builtin tuple type whose elements are all
`!felt.type`. Multiplicity is not part of the declaration; it remains a
per-use operand on `channel.push` and `channel.pull`.

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Some of this is repeated from the dialect description.

equality constraints across interacting LLZK structs. A channel represents
an unordered multiset of row-local tuples rather than an ordered stream.
The payload signature is declared explicitly on the channel definition. In
this task, the signature is a builtin tuple type whose elements are all

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

"In this task" sounds odd.

class ChannelUseOpBase<string mnemonic, list<Trait> traits = []>
: ChannelDialectOp<
mnemonic, traits#[AttrSizedOperandSegments, ConstraintGen,
DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We might want to consider these to be memory-modifying ops with a memory effects trait.

Comment on lines +81 to +90
if (!rhs.tableOffset) {
return success();
}
if (!lhs.tableOffset) {
lhs = rhs;
return success();
}
if (lhs == rhs) {
return success();
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
if (!rhs.tableOffset) {
return success();
}
if (!lhs.tableOffset) {
lhs = rhs;
return success();
}
if (lhs == rhs) {
return success();
}
if (!rhs.tableOffset || lhs == rhs) {
return success();
}
if (!lhs.tableOffset) {
lhs = rhs;
return success();
}

Comment on lines +130 to +137
if (!rhs) {
out = lhs;
return success();
}
if (*lhs == *rhs) {
out = lhs;
return success();
}

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
if (!rhs) {
out = lhs;
return success();
}
if (*lhs == *rhs) {
out = lhs;
return success();
}
if (!rhs || *lhs == *rhs) {
out = lhs;
return success();
}

@iangneal
iangneal requested a review from a team May 26, 2026 18:04
```
}];

let arguments = (ins SymbolNameAttr:$sym_name, TypeAttr:$message_type);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Try TypeAttrOf<TupleOf<[LLZK_FeltType]> to get automatic verification

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Alternatively, since it must be a tuple of felt, maybe the channel def could just specify an IndexAttr to denote the size of the tuple and reduce IR verbosity

mnemonic, traits#[AttrSizedOperandSegments, ConstraintGen,
DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
let arguments = (ins FlatSymbolRefAttr:$channel_ref,
Variadic<AnyLLZKType>:$tuple, Optional<AnyLLZKType>:$mult);

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Based on your impl of the channel def and manually implemented verifier for mult I think these should both specify just felt type values are allowed.

Suggested change
Variadic<AnyLLZKType>:$tuple, Optional<AnyLLZKType>:$mult);
Variadic<LLZK_FeltType>:$tuple, Optional<LLZK_FeltType>:$mult);

Comment on lines +84 to +85
// expected-error@+1 {{'channel.push' op only valid within a 'function.def' with 'function.allow_constraint' attribute}}
channel.push @c (%x) : !felt.type

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

add same test for pull as well

function.def @emit(%a: !struct.type<@RowA>, %b: !struct.type<@RowB>) attributes {function.allow_constraint} {
%x = struct.readm %a[@x] : !struct.type<@RowA>, !felt.type
%y = struct.readm %b[@y] : !struct.type<@RowB>, !felt.type
// expected-error@+1 {{'channel.push' op tuple operands must be derived from a single row context}}

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

What is "row context", a struct? Error message could be more helpful if in terms of LLZK concepts.

DeclareOpInterfaceMethods<SymbolUserOpInterface>]> {
let arguments = (ins FlatSymbolRefAttr:$channel_ref,
Variadic<AnyLLZKType>:$tuple, Optional<AnyLLZKType>:$mult);
let hasCustomAssemblyFormat = 1;

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

why did let assemblyFormat = not work for these ops?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants