Session-types simulation of a QUIC-subset

I decided to make a graduation work in both field of Communication/Electronics
and type theory/programming language/category theory. Inspired by deep talk with LLM,
too lucky was I to find the field of session type! Then I was searching for books on
it. It's a bit young field, and with the unpopularity just within programming
languages, I just found one book Session Types by Simon J.Gay. But that's the time
when I don't even know about typed lambda calulus system, so I immediately went to
the first two chapter of Practical Foundation of Programming Languages by Robert
Harper. It took me about a whole month to have a taste of typed language system.

Then, Good Job! I spent another month on the first three chapters of Session Types.
The Type Safe Proofs takes really much intelligence to understand, but I overcome. Aha~
However I got a little bit lost. I couldn't make something to verify such type theories.

My most familiar language is Rust, so I googled "session types rust", then there come
the work by Philip Munksgaard first -- Session Types for Rust. The time is precious.
I thought I don't have enough time and ability to make a new DSL and use it. So I dicided
to choose this crate and make somthing out. Protocol? I found the QUIC maybe a good one.
It sounds novel! Why not simulate it out!

Quickstart

Requires Rust ≥ 1.85 (edition 2024).

git clone <this-repo> && cd quic-session-types

Run the examples:

# Full QUIC lifecycle (handshake → stream data → graceful close), in-memory channels
cargo run --example full_lifecycle

# Multiple concurrent streams over session-typed channels
cargo run --example multi_stream

# Same lifecycle relayed over real UDP sockets (localhost)
cargo run --example udp_lifecycle

Run the tests:

# Unit tests (55 tests covering frames, encoding, protocol logic)
cargo test --lib

# Compile-fail tests — verify that protocol violations are caught at compile time
cargo test --test protocol_violation