Enum GlobalType 

pub enum GlobalType {
    End,
    Comm {
        sender: String,
        receiver: String,
        branches: Vec<(Label, GlobalType)>,
    },
    Mu {
        var: String,
        body: Box<GlobalType>,
    },
    Var(String),
}

Global types describe protocols from the bird’s-eye view.

Corresponds to Lean’s GlobalType inductive type.

Syntax

• End: Protocol termination
• Comm { sender, receiver, branches }: Communication with labeled branches
• Mu { var, body }: Recursive type μt.G
• Var(t): Type variable reference

The Comm variant models p → q : {l₁(S₁).G₁, l₂(S₂).G₂, ...} where the sender p chooses which branch to take.

Examples

use telltale_types::{GlobalType, Label};

// Simple protocol: A -> B: hello. end
let g = GlobalType::send("A", "B", Label::new("hello"), GlobalType::End);
assert!(g.well_formed());

// Recursive protocol: μt. A -> B: msg. t
let rec = GlobalType::mu(
    "t",
    GlobalType::send("A", "B", Label::new("msg"), GlobalType::var("t")),
);
assert!(rec.well_formed());

Variants

End

Protocol termination

Comm

Communication: sender → receiver with choice of labeled continuations

Fields

sender: String

receiver: String

branches: Vec<(Label, GlobalType)>

Mu

Recursive type: μt.G binds variable t in body G

Fields

var: String

body: Box<GlobalType>

Var(String)

Type variable: reference to enclosing μ-binder

Implementations

impl GlobalType

pub fn send( sender: impl Into<String>, receiver: impl Into<String>, label: Label, cont: GlobalType, ) -> GlobalType

Create a simple send without choice

pub fn comm( sender: impl Into<String>, receiver: impl Into<String>, branches: Vec<(Label, GlobalType)>, ) -> GlobalType

Create a communication with multiple branches

pub fn mu(var: impl Into<String>, body: GlobalType) -> GlobalType

Create a recursive type

pub fn var(name: impl Into<String>) -> GlobalType

Create a type variable

pub fn roles(&self) -> Vec<String>

Extract all role names from this global type.

Corresponds to Lean’s GlobalType.roles.

pub fn free_vars(&self) -> Vec<String>

Extract free type variables from this global type.

Corresponds to Lean’s GlobalType.freeVars.

pub fn substitute(&self, var_name: &str, replacement: &GlobalType) -> GlobalType

Substitute a global type for a variable.

Corresponds to Lean’s GlobalType.substitute.

pub fn unfold(&self) -> GlobalType

Unfold one level of recursion: μt.G ↦ G[μt.G/t]

Corresponds to Lean’s GlobalType.unfold.

pub fn all_vars_bound(&self) -> bool

Check if all recursion variables are bound.

Corresponds to Lean’s GlobalType.allVarsBound.

pub fn all_comms_non_empty(&self) -> bool

Check if each communication has at least one branch.

Corresponds to Lean’s GlobalType.allCommsNonEmpty.

pub fn unique_branch_labels(&self) -> bool

Check if all communication nodes have unique branch label names.

pub fn no_self_comm(&self) -> bool

Check if sender and receiver are different in each communication.

Corresponds to Lean’s GlobalType.noSelfComm.

pub fn well_formed(&self) -> bool

Well-formedness predicate for global types.

Corresponds to Lean’s GlobalType.wellFormed. A global type is well-formed if:

1. All recursion variables are bound
2. Each communication has at least one branch
3. Sender ≠ receiver in each communication
4. All recursion is guarded (no immediate recursion without communication)

pub fn mentions_role(&self, role: &str) -> bool

Check if a role participates in the global type.

Corresponds to Lean’s GlobalType.mentionsRole.

pub fn depth(&self) -> usize

Count the depth of a global type (for termination proofs).

Corresponds to Lean’s GlobalType.depth.

pub fn is_guarded(&self) -> bool

Check if a global type is guarded (no immediate recursion without communication).

Corresponds to Lean’s GlobalType.isGuarded.

pub fn consume( &self, sender: &str, receiver: &str, label: &str, ) -> Option<GlobalType>

Consume a communication from a global type.

Corresponds to Lean’s GlobalType.consume. G \ p →ℓ q represents the global type after the communication p →ℓ q has been performed.

Trait Implementations

impl Clone for GlobalType

fn clone(&self) -> GlobalType

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Contentable for GlobalType

fn to_bytes(&self) -> Result<Vec<u8>, ContentableError>

Serialize to canonical byte representation (JSON format).

fn to_template_bytes(&self) -> Result<Vec<u8>, ContentableError>

Serialize to template bytes, allowing open terms with explicit free-variable interfaces when supported by the implementation.

fn from_bytes(bytes: &[u8]) -> Result<GlobalType, ContentableError>

Deserialize from JSON bytes.

fn from_bytes_verified<H>( bytes: &[u8], expected: &ContentId<H>, ) -> Result<Self, ContentableError>

where H: Hasher,

Verify the content ID before deserializing from JSON bytes.

fn content_id<H>(&self) -> Result<ContentId<H>, ContentableError>

where H: Hasher,

Compute content ID using the specified hasher (from JSON bytes).

fn content_id_default(&self) -> Result<ContentId, ContentableError>

Compute content ID using the central default content hasher (from JSON bytes).

fn content_id_blake3(&self) -> Result<ContentId, ContentableError>

Compute content ID using explicit BLAKE3 (from JSON bytes).

fn template_id<H>(&self) -> Result<ContentId<H>, ContentableError>

where H: Hasher,

Compute a template ID using the specified hasher (from template bytes).

fn template_id_default(&self) -> Result<ContentId, ContentableError>

Compute a template ID using the central default content hasher.

fn template_id_blake3(&self) -> Result<ContentId, ContentableError>

Compute a template ID using explicit BLAKE3.

impl Debug for GlobalType

fn fmt(&self, f: &mut Formatter<'_>) -> Result<(), Error>

Formats the value using the given formatter.

impl<'de> Deserialize<'de> for GlobalType

fn deserialize<__D>( __deserializer: __D, ) -> Result<GlobalType, <__D as Deserializer<'de>>::Error>

where __D: Deserializer<'de>,

Deserialize this value from the given Serde deserializer.

impl Hash for GlobalType

fn hash<__H>(&self, state: &mut __H)

where __H: Hasher,

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq for GlobalType

fn eq(&self, other: &GlobalType) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Serialize for GlobalType

fn serialize<__S>( &self, __serializer: __S, ) -> Result<<__S as Serializer>::Ok, <__S as Serializer>::Error>

where __S: Serializer,

Serialize this value into the given Serde serializer.

impl Eq for GlobalType

impl StructuralPartialEq for GlobalType