EasyCrypt · fdupress · Jun 18, 2026
diff --git a/config/tests.config b/config/tests.config
@@ -13,5 +13,8 @@ exclude = examples/MEE-CBC examples/old examples/old/list-ddh !examples/incomple
 [test-mee-cbc]
 okdirs = examples/MEE-CBC
 
+[test-tutorials]
+okdirs = !doc/tutorials
+
 [test-unit]
 okdirs = tests tests/exception
diff --git a/doc/conf.py b/doc/conf.py
@@ -15,7 +15,7 @@
 # -- Project information -----------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#project-information
 
-project = 'EasyCrypt refman'
+project = 'EasyCrypt Documentation'
 copyright = '2026, EasyCrypt development team'
 author = 'EasyCrypt development team'
 

diff --git a/doc/index.rst b/doc/index.rst
@@ -1,7 +1,8 @@
-EasyCrypt reference manual
+EasyCrypt Documentation
 ========================================================================
 
 .. toctree::
    :maxdepth: 2
 
-   tactics
+   tutorials
+   reference
diff --git a/doc/reference.rst b/doc/reference.rst
@@ -0,0 +1,8 @@
+Reference Material
+========================================================================
+
+.. toctree::
+   :maxdepth: 1
+   :glob:
+
+   reference/*
diff --git a/doc/tactics.rst → doc/reference/tactics.rst b/doc/tactics.rst → doc/reference/tactics.rst
diff --git a/doc/tactics/async-while.rst → doc/reference/tactics/async-while.rst b/doc/tactics/async-while.rst → doc/reference/tactics/async-while.rst
diff --git a/doc/tactics/cfold.rst → doc/reference/tactics/cfold.rst b/doc/tactics/cfold.rst → doc/reference/tactics/cfold.rst
diff --git a/doc/tactics/clear.rst → doc/reference/tactics/clear.rst b/doc/tactics/clear.rst → doc/reference/tactics/clear.rst
diff --git a/doc/tactics/hoare-split.rst → doc/reference/tactics/hoare-split.rst b/doc/tactics/hoare-split.rst → doc/reference/tactics/hoare-split.rst
diff --git a/doc/tactics/if.rst → doc/reference/tactics/if.rst b/doc/tactics/if.rst → doc/reference/tactics/if.rst
diff --git a/doc/tactics/proc.rst → doc/reference/tactics/proc.rst b/doc/tactics/proc.rst → doc/reference/tactics/proc.rst
diff --git a/doc/tactics/procstar.rst → doc/reference/tactics/procstar.rst b/doc/tactics/procstar.rst → doc/reference/tactics/procstar.rst
diff --git a/doc/tactics/rnd.rst → doc/reference/tactics/rnd.rst b/doc/tactics/rnd.rst → doc/reference/tactics/rnd.rst
diff --git a/doc/tactics/simplify-if.rst → doc/reference/tactics/simplify-if.rst b/doc/tactics/simplify-if.rst → doc/reference/tactics/simplify-if.rst
diff --git a/doc/tactics/skip.rst → doc/reference/tactics/skip.rst b/doc/tactics/skip.rst → doc/reference/tactics/skip.rst
diff --git a/doc/tactics/splitwhile.rst → doc/reference/tactics/splitwhile.rst b/doc/tactics/splitwhile.rst → doc/reference/tactics/splitwhile.rst
diff --git a/doc/tactics/swap.rst → doc/reference/tactics/swap.rst b/doc/tactics/swap.rst → doc/reference/tactics/swap.rst
diff --git a/doc/tutorials.rst b/doc/tutorials.rst
@@ -0,0 +1,10 @@
+Tutorials
+========================================================================
+
+.. toctree::
+   :maxdepth: 0
+   :glob:
+
+  tutorials/tutorials.rst
+  tutorials/introduction-itp-program-logics.rst
+  tutorials/encryption-from-prf.rst
diff --git a/doc/tutorials/encryption-from-prf.rst b/doc/tutorials/encryption-from-prf.rst
@@ -0,0 +1,16 @@
+Encryption from a PRF
+=====================
+
+As a warm-up, we’ll consider a simple nonce-based symmetric encryption
+scheme for fixed-length messages. [1]_ Here, we assume some familiarity
+with cryptographic definitions and proofs, but not with the specific
+definitions and proofs used in this tutorial.
+
+You may find it beneficial to step through the `proof
+file </docs/tutorials/encryption-from-prf/Construction.eca>`__ as you
+read through the basic tutorial. The “Going Further” tutorials each come
+with their own proof files, referred to where relevant.
+
+.. [1]
+   Note the similarities to The Joy of Cryptography’s `Construction
+   7.4 <https://joyofcryptography.com/pdf/chap7.pdf#page=7>`__.