diff --git a/lean/Spa/Language/Semantics.lean b/lean/Spa/Language/Semantics.lean
index e2e6633..19a3925 100644
--- a/lean/Spa/Language/Semantics.lean
+++ b/lean/Spa/Language/Semantics.lean
@@ -51,6 +51,8 @@ inductive EvalBasicStmt : Env → BasicStmt → Env → Type
   | assign (ρ : Env) (x : String) (e : Expr) (v : Value) :
       EvalExpr ρ e v → EvalBasicStmt ρ (.assign x e) ((x, v) :: ρ)
 
+/-- Inference rules for evaluating a basic-statement-or-nothing,
+    which is the current representation of CFGs nodes. -/
 inductive EvalBasicStmtOpt : Env → Option BasicStmt → Env → Type
   | none {ρ : Env} : EvalBasicStmtOpt ρ Option.none ρ
   | some {ρ₁ ρ₂ : Env} {bs : BasicStmt} :
diff --git a/lean/Spa/Language/Traces.lean b/lean/Spa/Language/Traces.lean
index 49ea6af..712f66a 100644
--- a/lean/Spa/Language/Traces.lean
+++ b/lean/Spa/Language/Traces.lean
@@ -1,8 +1,34 @@
 import Spa.Language.Semantics
 import Spa.Language.Graphs
 
+/-!
+
+# Program Traces
+
+This module defines program traces tied to Control Flow Graphs, or CFGs
+(see `Spa.GGraph` and `Spa.Graph`). These traces boil town to sequences of
+basic-block executions (really, `Spa.BasicStmt` executions), each of which must
+have an actual basic block in the graph _and_ be connected to the previous
+basic block by an edge. In this way, traces encode executions admitted
+by the CFG.
+
+While the regular `Trace` is just _any_ path through the graph, an
+`EndToEndTrace` is a path from the entry node to the exit node, denoting
+full program execution.
+
+Properties about graphs and language semantics (especially,
+the fact that the graph contains the proper basic block and edges
+to represent any program execution according to the
+language's big-step semantics `EvalStmt`) is found
+in `Spa/Language/Properties.lean`.
+
+-/
+
 namespace Spa
 
+/-- A partial trace through a graph `g`, starting right before
+    the execution of the basic block at the first index, and
+    ending right after the execution of the basic block at the last index. -/
 inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
   | single {ρ₁ ρ₂ : Env} {idx : g.Index} :
       EvalBasicStmtOpt ρ₁ (g.nodes idx) ρ₂ → Trace g idx idx ρ₁ ρ₂
@@ -10,6 +36,10 @@ inductive Trace (g : Graph) : g.Index → g.Index → Env → Env → Type
       EvalBasicStmtOpt ρ₁ (g.nodes idx₁) ρ₂ → (idx₁, idx₂) ∈ g.edges →
       Trace g idx₂ idx₃ ρ₂ ρ₃ → Trace g idx₁ idx₃ ρ₁ ρ₃
 
+/-- Sequence two traces together. Since the endpoint of the first trace
+    is _after_ its last basic block's execution, and the beginning of
+    the next trace is _before_ its first basic block's execution,
+    there must be an edge to connect the two. -/
 noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Index}
     {ρ₁ ρ₂ ρ₃ : Env} (tr₁ : Trace g idx₁ idx₂ ρ₁ ρ₂)
     (he : (idx₂, idx₃) ∈ g.edges) (tr₂ : Trace g idx₃ idx₄ ρ₂ ρ₃) :
@@ -18,6 +48,7 @@ noncomputable def Trace.concat {g : Graph} {idx₁ idx₂ idx₃ idx₄ : g.Inde
   | single hbs => exact Trace.edge hbs he tr₂
   | edge hbs he' _ ih => exact Trace.edge hbs he' (ih he tr₂)
 
+/-- A beginning-to-end trace corresponding to the CFG `g`. -/
 inductive EndToEndTrace (g : Graph) (ρ₁ ρ₂ : Env) : Type
   | intro (idx₁ : g.Index) (idx₁_mem : idx₁ ∈ g.inputs)
       (idx₂ : g.Index) (idx₂_mem : idx₂ ∈ g.outputs)