diff --git a/lib/pulse/lib/class/Pulse.Class.Small.fst b/lib/pulse/lib/class/Pulse.Class.Small.fst
new file mode 100644
index 000000000..27abd0d39
--- /dev/null
+++ b/lib/pulse/lib/class/Pulse.Class.Small.fst
@@ -0,0 +1,26 @@
+module Pulse.Class.Small
+
+open Pulse.Lib.Pervasives
+
+instance small_emp : small emp = {
+  pf = ();
+}
+
+instance small_star
+  (p q : vprop)
+  (sp : small p)
+  (sq : small q)
+  : small (p ** q) = {
+  pf = ();
+}
+
+instance small_pure
+  (p : prop)
+  : small (pure p) = {
+  pf = ();
+}
+
+let small_from_small_ref (v:vprop) (_ : squash (is_small v))
+  : small v = {
+  pf = ();
+}
diff --git a/lib/pulse/lib/class/Pulse.Class.Small.fsti b/lib/pulse/lib/class/Pulse.Class.Small.fsti
new file mode 100644
index 000000000..a7087f230
--- /dev/null
+++ b/lib/pulse/lib/class/Pulse.Class.Small.fsti
@@ -0,0 +1,20 @@
+module Pulse.Class.Small
+
+open Pulse.Lib.Pervasives
+
+class small (v : vprop) = {
+  pf : squash (is_small v);
+}
+
+instance val small_emp : small emp
+
+instance val small_star
+  (p q : vprop)
+  (sp : small p)
+  (sq : small q) : small (p ** q)
+
+instance val small_pure (p : prop) : small (pure p)
+
+(* Intentionally not an instance. *)
+val small_from_small_ref (v:vprop) (_ : squash (is_small v))
+  : small v