cleanup: move all TreeSync symbolic state in a separate namespace

Inria-Prosecco · Oct 24, 2024 · 245321b · 245321b
1 parent bb5014f
commit 245321b
Show file tree

Hide file tree

Showing 9 changed files with 17 additions and 17 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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/...LS.TreeSync.Symbolic.AuthServiceCache.fst → ...eSync.Symbolic.State.AuthServiceCache.fst b/...LS.TreeSync.Symbolic.AuthServiceCache.fst → ...eSync.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/...LS.TreeSync.Symbolic.API.GroupManager.fst → ....TreeSync.Symbolic.State.GroupManager.fst b/...LS.TreeSync.Symbolic.API.GroupManager.fst → ....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/...eeSync.Symbolic.API.KeyPackageManager.fst → ...Sync.Symbolic.State.KeyPackageManager.fst b/...eeSync.Symbolic.API.KeyPackageManager.fst → ...Sync.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/...S.TreeSync.Symbolic.SignatureKeyState.fst → ....TreeSync.Symbolic.State.SignatureKey.fst b/...S.TreeSync.Symbolic.SignatureKeyState.fst → ....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/...ic/MLS.TreeSync.Symbolic.API.Sessions.fst → ...olic/MLS.TreeSync.Symbolic.State.Tree.fst b/...ic/MLS.TreeSync.Symbolic.API.Sessions.fst → ...olic/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