Module execution_hints 

Execution hints for code generation (deployment-level concerns) Execution Hints for Choreographic Protocols

This module defines execution hints that are extracted from choreography annotations and used during code generation. Hints are separate from the pure session types (LocalType) to maintain Lean correspondence.

Design Rationale

Annotations like @parallel and @min_responses(N) are deployment concerns, not protocol semantics. Keeping them separate from LocalType:

• Preserves Lean correspondence (LocalType matches LocalTypeR)
• Aligns with spatial type theory (Intent vs Deployment layers)
• Allows hints to evolve independently of type theory

Architecture

Choreography AST                    ExecutionHints
(with annotations)                  (extracted separately)
       │                                   │
       │ projection                        │ (passed through)
       ▼                                   ▼
   LocalType              +          ExecutionHints
  (pure types)                      (keyed by path)
       │                                   │
       └──────────────┬────────────────────┘
                      │ codegen
                      ▼
              Generated Code
         (consults hints for parallel)

Structs

ChoreographyWithHints

A choreography paired with its extracted execution hints.

ExecutionHints

Collection of execution hints for a protocol.

ExecutionHintsBuilder

Builder for constructing ExecutionHints.

OperationHints

Execution hints for a single operation.

OperationPath

Path to an operation in the local type tree.

Enums

OperationStep

A step in the path to an operation within a local type tree.