From 245321b9c39750c5f1869c20afa2c4b6416e2da5 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Th=C3=A9ophile=20Wallez?= Date: Thu, 24 Oct 2024 09:56:48 +0200 Subject: [PATCH] cleanup: move all TreeSync symbolic state in a separate namespace --- fstar/treesync/symbolic/MLS.TreeSync.Symbolic.API.fst | 10 +++++----- .../symbolic/MLS.TreeSync.Symbolic.AuthService.fst | 2 +- .../symbolic/MLS.TreeSync.Symbolic.GlobalUsage.fst | 10 +++++----- .../MLS.TreeSync.Symbolic.LeafNodeSignature.fst | 2 +- ...> MLS.TreeSync.Symbolic.State.AuthServiceCache.fst} | 2 +- ...st => MLS.TreeSync.Symbolic.State.GroupManager.fst} | 2 +- ... MLS.TreeSync.Symbolic.State.KeyPackageManager.fst} | 2 +- ...st => MLS.TreeSync.Symbolic.State.SignatureKey.fst} | 2 +- ...ssions.fst => MLS.TreeSync.Symbolic.State.Tree.fst} | 2 +- 9 files changed, 17 insertions(+), 17 deletions(-) rename fstar/treesync/symbolic/{MLS.TreeSync.Symbolic.AuthServiceCache.fst => MLS.TreeSync.Symbolic.State.AuthServiceCache.fst} (97%) rename fstar/treesync/symbolic/{MLS.TreeSync.Symbolic.API.GroupManager.fst => MLS.TreeSync.Symbolic.State.GroupManager.fst} (97%) rename fstar/treesync/symbolic/{MLS.TreeSync.Symbolic.API.KeyPackageManager.fst => MLS.TreeSync.Symbolic.State.KeyPackageManager.fst} (97%) rename fstar/treesync/symbolic/{MLS.TreeSync.Symbolic.SignatureKeyState.fst => MLS.TreeSync.Symbolic.State.SignatureKey.fst} (99%) rename fstar/treesync/symbolic/{MLS.TreeSync.Symbolic.API.Sessions.fst => MLS.TreeSync.Symbolic.State.Tree.fst} (99%) 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