CS 242: Assignment 8: Typestate

Due: Friday, November 22 at 11:59pm
Submission cutoff: Monday, November 25 at 11:59pm

In this assignment, you will work with state machines and communication protocols in Rust. First, you will implement a simple shopping cart state machine and generate test cases. Then you will implement a basic session-typed TCP library.

1: Shopping cart (50%)

Stateful web applications are a fruitful domain for modeling with state machines. Sergio Benitez, creator of Rocket and Stanford PhD student, gave a talk in this class last year about using typestate in Rust to build safer web servers. Let’s say that you’re tasked with implementing a web backend for a simple shopping cart application. Your software architect handed you the following state machine diagram:

They also handed gave you test cases in tests/cart.rs like this one:

#[test]
fn order_test() {
  // Get a cart after logging in
  let empty = Cart::login(
    "username".to_string(), "password".to_string()).unwrap();
  // Cart becomes non empty after first item
  let nonempty = empty.additem(1.0);
  // Can continue adding items to cart
  let nonempty = nonempty.additem(1.0);
  // Checkout freezes cart from adding more items
  let checkout = nonempty.checkout();
  // After attempting to order, we either succeed and get back an
  // empty cart, or get an error and keep the checkout cart.
  match checkout.order() {
    Ok(cart) => {
      let _ = cart.additem(1.0);
    }
    Err((cart, err)) => {
      println!("{}", err);
      let _ = cart.order();
    }
  }
}

1.1: Cart API (30%)

In src/cart.rs, your task is to use the typestate pattern to design a shopping cart API that enforces the transitions of the state machine. Like with UseCounter in the previous assignment, you can design the interface however you want so long as it type-checks and runs correctly for the provided test cases.

A few notes on the design:

To authenticate a user and place an order, you must use an external API providedin src/backend.rs.
The only two methods in the cart API with a non-self parameter are login and additem. login takes a username and a password, and additem takes a cost of an item as an f64 (64-bit float). When you place an order, you should submit the total cost of all the items in the cart.
You can either use a polymorphic state design (e.g. Cart<S>) or a separate-struct state design (e.g. struct Empty { .. }; struct Nonempty { .. };). Up to you!

To run the provided tests (all of which should compile), you can run cargo test.

1.2: Compile-fail tests (20%)

As a means of testing the correctness of your implementation, you should write a series of tests that attempt to use the cart API in an incorrect way. Here’s a basic example in tests/cart-fail/fail1.rs:

extern crate assign8;
use assign8::cart::*;

fn main() {
  let empty = Cart::login("A".into(), "B".into()).unwrap();
  empty.checkout();
}

Here, the checkout method should not be available on an empty cart. By the typestate design, this should be a compile-time error and the code should not compile. Your task is to create more tests for different potential abuses of the API (see the typestate lecture for what classes of errors to think about). Each test should be a separate file in the tests/cart-fail directory, which will be executed by the cart_fail test in tests/cart.rs.

To evaluate the quality of your tests, we have created several hidden implementatiosn of the cart API that fail to implement the specification correctly. Your tests will receive points proportional to the number of implementations in which they can demonstrate the flaw.

Demonstrating a flaw means a test compiles when it should not under a correct implementation. For example, the test above would succeed compiling against this incorrect API:

struct Cart;

impl Cart {
  pub fn login(...) -> Result<Cart, ...> { ... }
  pub fn checkout(...) -> Result<Cart, ...> { ... }
}

Upload your solution to Gradescope to see whether your test coverage gets all the bugs. The autograder will be available shortly after the assignment is released.

2. Verified TCP (50%)

Next, your main challenge for this assignment is to implement a simplified, session-typed version of the TCP protocol. Before we dive into that, we first need to introduce one last session typing concept, which is the implementation of recursive session types.

2.1: Recursive session types

In the lecture notes, we show how in their theoretical formulation, session types are allowed to be recursive. For example, here’s a protocol for an infinite echo server:

$\begin{align*} \msf{Server} &= \srec{\sigma}{\srecv{\msf{String}}{\soffer{\msf{loop}}{\sigma}{\msf{quit}}{\eps}}} \\ \msf{Client} = \dual{\msf{Server}} &= \srec{\sigma}{\ssend{\msf{String}}{\schoose{\msf{loop}}{\sigma}{\msf{quit}}{\eps}}} \end{align*}$

To implement this in Rust, we need to introduce a notion of recursion points and type variables, i.e. the $\mu~\sigma$ and $\sigma$ parts. Representing variables in our type system is a tricky problem, but we can simplify by avoiding names entirely and instead using de Bruijn indices. This is the same convention you saw with numbered label scopes in WebAssembly—the number 0 refers to the closest recursion point, 1 refers to the next up, and so on.

This reduces our problem to: how do we write numbers in Rust’s type system? And for that, we will use the Peano numerals, the same construction you saw on assignment 1 in the lambda calculus Church encoding. Specifically we have four new types:

pub struct Rec<S>(PhantomData<S>);
pub struct Z;
pub struct S<N>(PhantomData<N>);
pub struct Var<N>(PhantomData<N>);

Here, Rec<S> represents a recursion point $\mu~\sigma$ . Z and S<N> are types representing Peano numerals, so S<S<S<Z>>> is the type corresponding to the number 3. Lastly, Var<N> represents a usage of a variable where N is a Peano number. For example, we can translate our echo server as:

type Server = Rec<Recv<String, Offer<Var<Z>, Close>>>;
type Client = <Server as HasDual>::Dual;

And we can implement this protocol:

fn server(c: Chan<(), Server>) {
  let mut c = c.rec_push();
  loop {
    c = {
      let (c, s) = c.recv();
      println!("{}", s);
      match c.offer() {
        Branch::Left(c) => c.rec_pop(),
        Branch::Right(c) => { c.close(); return; }
      }
    }
  }
}

fn client(c: Chan<(), Client>) {
  let mut c = c.rec_push();
  loop {
    c = {
      let c = c.send("echo!".to_string());
      c.left().rec_pop()
    }
  }
}

A few key differences from before. First, our Chan type now has two arguments: an environment Env and a session type S. The environment is similar to the proof context $\ctx$ in that it represents a mapping from variables (numbers) to session types. At the start of our protocol, the environment is empty, represented by the unit type ().

Second, channels with outermost session type Rec and Var expose two methods: rec_push() and rec_pop(), respectively. rec_push() means “enter a recursive session”, and rec_pop() means “leave a recursive session”. Multiple rec_pop calls can return across multiple nested recursions. Effectively, rec_push puts the current session type onto the Env stack, and rec_pop removes it from the stack. To implement this, we add the following Chan implementations:

impl<Env, S> Chan<Env, Rec<S>> {
  pub fn rec_push(self) -> Chan<(S, Env), S> {
    unsafe { transmute(self) }
  }
}

impl<Env, S> Chan<(S, Env), Var<Z>> {
  pub fn rec_pop(self) -> Chan<(S, Env), S> {
    unsafe { transmute(self) }
  }
}

impl<Env, S, N> Chan<(S, Env), Var<S<N>>> {
  pub fn rec_pop(self) -> Chan<Env, Var<N>> {
    unsafe { transmute(self) }
  }
}

For another example, we have extended the ATM example from class to use recursive session types in src/atm.rs.

2.2: TCP

Now that you have the full power of session types at your fingertips, it’s time to talk networking. TCP, or the Transmission Control Protocol, is a communication protocol that defines a means to reliably transmit bytes over a network connection. We are going to define a protocol that looks loosely like TCP that you are going to implement using session types in Rust. The three core components of the protocol are the handshake, data transfer, and close. We are assuming unidirectional data transfer (from the client to the server).

Handshake: a handshake is a sequence of three messages, a Syn, SynAck, and Ack. Specifically, we have the following types:
```
struct Syn;
struct SynAck;
struct Ack;
```
The server receives a Syn, responds with a SynAck, receives an Ack, then enters the data transfer phase.
Data transfer: the payload is a series of buffers that the client will attempt to transfer to the server. The client sends each buffer in a Packet objects along with the buffer’s sequence number (which, for our purposes, is just its index in a list of packets the client wants to send). The server will receive some (but not necessarily all) of these packets (i.e. Vec<Packet>), and respond with the list of buffer sequence numbers received (i.e. Vec<usize>). Then the server will offer to enter the close phase if all the packets have been received, otherwise restart the data transfer process.
```
type Buffer = Vec<u8>;

struct Packet {
  buf: Buffer,
  seqno: usize
}
```
Note: the two types above are actually defined in session.rs to enable our noisy channel implementation, mentioned below.
Close: once the client requests to close the connection, the server will send an Ack and then a Fin, receive a final Ack from the client, and then close the connection at the end of this sequence.

Here is an example of a possible session where the client wants to send three buffers. Curly braces are used to indicate an ordered sequence of values. Note that “Choose close” would normally be a “Fin” in TCP, but in your session type should be a Offer<..., TCPClose> branch (on the server), not a Recv<Fin, ...>.

Given this specification, your task is to implement the following:

type TCPHandshake = /* TODO */
type TCPRecv = /* TODO */
type TCPClose = /* TODO */
type TCPServer = TCPHandshake<TCPRecv<TCPClose>>;
type TCPClient = <TCPServer as HasDual>::Dual;

fn tcp_server(c: Chan<(), TCPServer>) -> Vec<Buffer>;
fn tcp_client(c: Chan<(), TCPClient>, packets: Vec<Buffer>);

First, uncomment the line // pub mod tcp in lib.rs.

Next, you should translate the English specification above into a session type TCPServer. We have helpfully suggested a possible decomposition of this type in src/tcp.rs.

Then, you should implement this session type in the tcp_server and tcp_client functions. tcp_server should return the list of received buffers in sorted order by sequence number.

Lastly, note that unlike a more robust TCP implementation, your protocol does not have to handle timeouts, SYN floods, or anything else. We are assuming the only point of failure is the packet transmission step, where packets can be dropped when sending from the client to the server.

2.3: Testing

We’ve given you two tests for your TCP implementation in lib.rs. One uses a standard implementation of Chan as in the session types lecture notes; one uses an implementation of Chan that drops packets with some probability, so that you can test your resend behavior. You can run these tests with cargo test (and cargo test -- --nocapture if you want to debug with print statements).

There should only be one correct implementation of the TCPServer and TCPClient types. When you upload your code to Gradescope, if you see a message in the autograder’s output that says your TCP type is wrong/uncompilable, then you should check your type implementation. If you see “Assignment graded”, that means your TCP type is correct (albeit with no guarantees on tests passing). The autograder will be available shortly after the assignment is released.

Submission

Run ./make_submission.sh and upload the generated assign8.zip to Gradescope.

Sections