diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
index bb5be1a..5c8ca8b 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst
@@ -14,13 +14,13 @@ open MLS.TreeSync.Invariants.AuthService
 open MLS.TreeSync.Proofs.ParentHashGuarantees
 open MLS.TreeSync.API
 open MLS.Symbolic
-open MLS.TreeSync.Symbolic.API.GroupManager
-open MLS.TreeSync.Symbolic.API.KeyPackageManager
-open MLS.TreeSync.Symbolic.API.Sessions
-open MLS.TreeSync.Symbolic.SignatureKeyState
+open MLS.TreeSync.Symbolic.State.GroupManager
+open MLS.TreeSync.Symbolic.State.KeyPackageManager
+open MLS.TreeSync.Symbolic.State.Tree
+open MLS.TreeSync.Symbolic.State.SignatureKey
+open MLS.TreeSync.Symbolic.State.AuthServiceCache
 open MLS.TreeSync.Symbolic.API.IsWellFormedInvariant
 open MLS.TreeSync.Symbolic.AuthService
-open MLS.TreeSync.Symbolic.AuthServiceCache
 open MLS.TreeSync.Symbolic.LeafNodeSignature
 open MLS.TreeSync.Symbolic.IsWellFormed
 open DY.Core
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst
index 6c67d75..582a7cb 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthService.fst
@@ -6,7 +6,7 @@ open DY.Lib
 open MLS.TreeSync.NetworkTypes
 open MLS.TreeSync.Invariants.AuthService
 open MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
-open MLS.TreeSync.Symbolic.SignatureKeyState
+open MLS.TreeSync.Symbolic.State.SignatureKey
 open MLS.Symbolic
 
 #set-options "--fuel 0 --ifuel 0"
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
index a901099..be5c37c 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst
@@ -8,11 +8,11 @@ open MLS.TreeSync.NetworkTypes
 open MLS.Symbolic
 open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.TreeSync.Symbolic.LeafNodeSignature
-open MLS.TreeSync.Symbolic.AuthServiceCache
-open MLS.TreeSync.Symbolic.API.Sessions
-open MLS.TreeSync.Symbolic.SignatureKeyState
-open MLS.TreeSync.Symbolic.API.GroupManager
-open MLS.TreeSync.Symbolic.API.KeyPackageManager
+open MLS.TreeSync.Symbolic.State.AuthServiceCache
+open MLS.TreeSync.Symbolic.State.Tree
+open MLS.TreeSync.Symbolic.State.SignatureKey
+open MLS.TreeSync.Symbolic.State.GroupManager
+open MLS.TreeSync.Symbolic.State.KeyPackageManager
 open MLS.TreeSync.Symbolic.API
 
 #set-options "--fuel 0 --ifuel 0"
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
index 022f370..a51ff45 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.LeafNodeSignature.fst
@@ -23,7 +23,7 @@ open MLS.TreeSync.Symbolic.IsWellFormed
 open MLS.TreeSync.Symbolic.Parsers
 open MLS.TreeSync.Symbolic.AuthService
 open MLS.TreeSync.Symbolic.AuthService.CredentialInterpretation
-open MLS.TreeSync.Symbolic.SignatureKeyState
+open MLS.TreeSync.Symbolic.State.SignatureKey
 open MLS.Crypto.Derived.Symbolic.SignWithLabel
 open MLS.Symbolic
 open MLS.Result
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst
similarity index 97%
rename from fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
rename to fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst
index 9b0a8f0..7f7e861 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.AuthServiceCache.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.AuthServiceCache.fst
@@ -1,4 +1,4 @@
-module MLS.TreeSync.Symbolic.AuthServiceCache
+module MLS.TreeSync.Symbolic.State.AuthServiceCache
 
 open Comparse
 open DY.Core
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst
similarity index 97%
rename from fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
rename to fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst
index 64df43b..83fdaae 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.GroupManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.GroupManager.fst
@@ -1,4 +1,4 @@
-module MLS.TreeSync.Symbolic.API.GroupManager
+module MLS.TreeSync.Symbolic.State.GroupManager
 
 open Comparse
 open DY.Core
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst
similarity index 97%
rename from fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
rename to fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst
index 7a1e2cc..cd486de 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.KeyPackageManager.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.KeyPackageManager.fst
@@ -1,4 +1,4 @@
-module MLS.TreeSync.Symbolic.API.KeyPackageManager
+module MLS.TreeSync.Symbolic.State.KeyPackageManager
 
 open Comparse
 open DY.Core
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.SignatureKeyState.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.SignatureKey.fst
similarity index 99%
rename from fstar/treesync/symbolic/MLS.TreeSync.Symbolic.SignatureKeyState.fst
rename to fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.SignatureKey.fst
index 5ae00e3..ed14b30 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.SignatureKeyState.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.SignatureKey.fst
@@ -1,4 +1,4 @@
-module MLS.TreeSync.Symbolic.SignatureKeyState
+module MLS.TreeSync.Symbolic.State.SignatureKey
 
 open Comparse
 open DY.Core
diff --git a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst
similarity index 99%
rename from fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
rename to fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst
index 760ecc5..866269a 100644
--- a/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.Sessions.fst
+++ b/fstar/treesync/symbolic/MLS.TreeSync.Symbolic.State.Tree.fst
@@ -1,4 +1,4 @@
-module MLS.TreeSync.Symbolic.API.Sessions
+module MLS.TreeSync.Symbolic.State.Tree
 
 open Comparse
 open DY.Core