Assignment 1: Rocq

This assignment has two purposes:

1. Learn how to use Rocq to prove theorems. This is a skill you'll build on and use to verify programs in the rest of the class, so it's important you put enough practice in now.
2. Practice with functional programs. This is a warm up to imperative and concurrent programs as well as useful on its own, since functional programs are often used in the specification of imperative programs.

Submitting

See submitting assignments on the assignment setup page.

The assignment is due Monday, Sep 29th at 11pm. However, you are welcome and encouraged to submit early with partial progress to keep me informed of how the class is doing. If you have questions, just mention them briefly in the Canvas submission so I know to look.

I would recommend aiming to finish part 0 by Tuesday, September 9th and part 1 by Monday, Sep 15th to be on track.

Part 0: setup

The assignment setup page has instructions on getting the sys-verif-fa25-proofs repo and installing Rocq. Follow those first.

Warning

You might run into unexpected difficulties with installing the software, so do it early and ask for help quickly if you get stuck. It isn't a goal of the class to teach you to install software, but it is necessary to make progress on anything else.

Part 1: Software Foundations exercises

We'll use the free online textbook Software Foundations to learn the basics of using the Rocq prover to prove theorems. You'll read its explanations and do the inline exercises.

See the SF assignment page for details on what parts you should finish and hand in.

Important

These chapters have a lot of small, easy exercises to get you practice. If you find anything difficult, come to office hours sooner rather than later to get it sorted out. If they're easy, note that proofs will become more difficult quickly after this.

Part 2: verifying functional programs

Finish the exercises in src/sys_verif/assignments/hw1/rocq_exercises.v. You can view a rendering of Assignment 1 part 2 as a reference.