feat(io): Interpreter for the I/O Dialect

[ArquintL]

Extends the Interpreter's state by a source of entropy and a network abstraction.
The source of entropy is supposed to be initialized before interpretation starts and allows operations like random number generation to consume random bytes from this source. As soon as no entropy is left, the behavior is UB.
The network abstraction holds the in-flight messages as a FIFO queue and recv consumes (& drops) the first message in the queue for the given receiver.

[Copilot]

🟡 Changes recommended

Io.interpretOp' handles a non-existent .address opcode and references non-existent properties.id, so the io.self interpretation is incorrect and likely won’t compile.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Pull request overview

This PR adds interpreter support for the io dialect by extending interpreter state with (1) an entropy source for io.rand and (2) a simple in-flight message queue for io.send/io.recv, and introduces an io address runtime value to represent !io.address at runtime.

Changes:

• Add RuntimeValue.ioAddr plus refinement support for !io.address.
• Extend MemoryState with EntropyState and NetworkState, and implement entropy/message operations plus Io.interpretOp' (self/send/recv/rand).
• Update/extend MLIR tests, including a new interpreter roundtrip test for io.send/io.recv.

File summaries

File	Description
Veir/RuntimeValue.lean	Adds ioAddr runtime value and string rendering.
Veir/Interpreter/Refinement/Basic.lean	Extends runtime refinement relation to cover ioAddr.
Veir/Interpreter/Refinement/Lemmas.lean	Adds lemma for extracting ioAddr from refinement evidence.
Veir/Interpreter/Basic.lean	Extends interpreter memory state and implements entropy/network + io op interpretation.
Test/IO/roundtrip.mlir	Updates IO IR test to use io.self.
Test/Interpreter/IO/roundtrip.mlir	Adds interpreter roundtrip test for io.send/io.recv.

Review details

• Files reviewed: 6/6 changed files
• Comments generated: 1
• Review effort level: Lite

---

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

[Copilot]

🟡 Changes recommended

The IO interpreter currently converts arbitrary-width len operands via truncating toUInt64, which can silently wrap large lengths instead of failing/UB.

Once you've addressed the issues Copilot identified, you can request another Copilot review.

Review details

Suppressed comments (1)

Veir/Interpreter/Basic.lean:1851

• len for io.rand is accepted as any integer width, but len.toNat.toUInt64 truncates values above UInt64.max. This can wrap the requested byte count instead of failing/UB.

    let [.addr addr, .int _ len] := operands.toList | none
    let .val len := len | Interp.ub
    let len := len.toNat.toUInt64

• Files reviewed: 5/5 changed files
• Comments generated: 3
• Review effort level: Lite