Midnight.Passport.Semantics

Attaches semantics to the architecture diagram via the standard free category + interpretation functors recipe:

• C_arch — the free strict monoidal category generated by the channels ArchChan (objects are wire lists over them) and the boxes ArchBox (morphisms) of the architecture. architectureᶜ is the architecture rebuilt in this category.
• Syntax functor syn : C_arch → FMTerm — the object-generator map chanName : ArchChan → String together with synBox, which sends each box to its named gen. Because the objects differ (ArchChan vs String), syn transports along chanName; it recovers the architecture term verbatim.
• Semantics generator data — each channel to a Channel and each ArchBox to a Machine. By the universal property of the free strict monoidal category this data induces a monoidal functor C_arch → Machine once the Machine category is packaged as such.

The diagram below is the image of architectureᶜ under the syntax functor (architectureˢ); it is rendered straight from that term — compiled to Graphviz DOT and laid out by dot — so it cannot drift from the definitions on this page.

{-# OPTIONS --safe #-}
 
module Midnight.Passport.Semantics where
 
open import Data.String using (String)
open import Data.List   using (List; []; _∷_; [_]; map; _++_)
open import Data.List.Properties using (map-++)
 
open import Categories.FreeStrictMonoidal using (module FreeStrictMonoidalHelper)
 
import Midnight.Passport.FMTerm as FM
 
import CategoricalCrypto.Channel.Core as Ch
import CategoricalCrypto.Machine.Core as Mc

        
      

1. Object generators: the architecture's channels

The objects of C_arch are freely generated by the channel names, enumerated as ArchChan: an object is a wire list over ArchChan, and the tensor is concatenation (Var/_⊗₀_/unit are the same sugar FMTerm provides over String).

data ArchChan : Set where
  TBD TBD-SYNC RECOVERY-P5 READ-STATE JUBJUB-SCHNORR STATE WITNESS-IPC CHAIN User : ArchChan
 
ObjTerm : Set
ObjTerm = List ArchChan
 
infixr  _⊗₀_
_⊗₀_ : ObjTerm → ObjTerm → ObjTerm
_⊗₀_ = _++_
 
unit : ObjTerm
unit = []
 
Var : ArchChan → ObjTerm
Var = [_]

        
      

2. Morphism generators: exactly the boxes of architecture

The morphism generators are the architecture's components — one ArchBox constructor per box, indexed by its domain and codomain object-terms. Restricting the generators to exactly these boxes is what makes C_arch the free category of the architecture (rather than of arbitrary named morphisms).

data ArchBox : ObjTerm → ObjTerm → Set where
  didContract     : ArchBox unit (Var TBD)
  nameService     : ArchBox unit (Var TBD)
  peerDevices     : ArchBox unit (Var TBD-SYNC)
  recoveryHelpers : ArchBox unit (Var RECOVERY-P5)
  indexer         : ArchBox unit (Var READ-STATE)
  accountCustody  : ArchBox (Var TBD ⊗₀ Var TBD ⊗₀ Var CHAIN) (Var JUBJUB-SCHNORR)
  localWallet     : ArchBox (Var TBD-SYNC) (Var STATE)
  proofServer     : ArchBox unit (Var WITNESS-IPC)
  passportKey     : ArchBox
                      ( Var RECOVERY-P5 ⊗₀ Var READ-STATE ⊗₀ Var JUBJUB-SCHNORR
                      ⊗₀ Var STATE ⊗₀ Var WITNESS-IPC )
                      ( Var User )
 
module HA = FreeStrictMonoidalHelper ArchBox; open HA

        
      

3. architecture, rebuilt in C_arch

The architecture itself is a single morphism CHAIN → User in C_arch: the blockchain enters at the bottom boundary (it is the environment's wire, read by accountCustody), and three layers of boxes are composed left-to-right, the CHAIN wire threading through the first.

architectureᶜ : WTerm (Var CHAIN) (Var User)
architectureᶜ =
    boxʷ passportKey
  ∘ʷ (    boxʷ recoveryHelpers ⊗ʷ boxʷ indexer ⊗ʷ boxʷ accountCustody
       ⊗ʷ boxʷ localWallet     ⊗ʷ boxʷ proofServer )
  ∘ʷ ( boxʷ didContract ⊗ʷ boxʷ nameService ⊗ʷ idʷ ⊗ʷ boxʷ peerDevices )

        
      

4. Syntax functor C_arch → FMTerm

The object part is Φ = map chanName; the morphism part is synBox, sending each box to the correspondingly-named gen. Since the two categories have different object generators (ArchChan vs String), the functor syn transports the object indices through chanName — the map-++ rewrites discharge that chanName distributes over the tensor. architectureˢ is the image of architectureᶜ; it is the term the diagram above is rendered from.

chanName : ArchChan → String
chanName TBD            = "TBD"
chanName TBD-SYNC       = "TBD SYNC"
chanName RECOVERY-P5    = "RECOVERY-P5"
chanName READ-STATE     = "READ STATE"
chanName JUBJUB-SCHNORR = "JUBJUB SCHNORR"
chanName STATE          = "STATE"
chanName WITNESS-IPC    = "WITNESS-IPC"
chanName CHAIN          = "CHAIN"
chanName User           = "User"
 
Φ : ObjTerm → FM.ObjTerm
Φ = map chanName
 
synBox : ∀ {A B} → ArchBox A B → FM.HomTerm (Φ A) (Φ B)
synBox didContract     = FM.gen "Midnight DID contract"   FM.unit (FM.Var "TBD")
synBox nameService     = FM.gen "Name Service"            FM.unit (FM.Var "TBD")
synBox peerDevices     = FM.gen "+ peer devices"          FM.unit (FM.Var "TBD SYNC")
synBox recoveryHelpers = FM.gen "Recovery helpers"        FM.unit (FM.Var "RECOVERY-P5")
synBox indexer         = FM.gen "Indexer"                 FM.unit (FM.Var "READ STATE")
synBox accountCustody  = FM.gen "Account custody contract"
                           (FM.Var "TBD" FM.⊗₀ FM.Var "TBD" FM.⊗₀ FM.Var "CHAIN")
                           (FM.Var "JUBJUB SCHNORR")
synBox localWallet     = FM.gen "Local wallet storage"    (FM.Var "TBD SYNC") (FM.Var "STATE")
synBox proofServer     = FM.gen "Proof server"            FM.unit (FM.Var "WITNESS-IPC")
synBox passportKey     = FM.gen "Passport Key"
                           ( FM.Var "RECOVERY-P5" FM.⊗₀ FM.Var "READ STATE" FM.⊗₀ FM.Var "JUBJUB SCHNORR"
                           FM.⊗₀ FM.Var "STATE" FM.⊗₀ FM.Var "WITNESS-IPC" )
                           ( FM.Var "User" )
 
syn : ∀ {A B} → WTerm A B → FM.HomTerm (Φ A) (Φ B)
syn (boxʷ b)  = synBox b
syn idʷ       = FM.id
syn (g ∘ʷ f)  = syn g FM.∘ syn f
syn (_⊗ʷ_ {A} {B} {C} {D} f g)
  rewrite map-++ chanName A C | map-++ chanName B D = syn f FM.⊗₁ syn g
 
architectureˢ : FM.HomTerm (FM.Var "CHAIN") (FM.Var "User")
architectureˢ = syn architectureᶜ

        
      

5. Semantics interpretation: generators → Machine

The semantics is given as generator data: a Channel per channel and a Machine per box. A ChannelModel fixes the objects (and lifts them to the functor's object map ⟦_⟧₀); a MachineModel fixes the machines and reads them off as the morphism map ⟦_⟧₁ : ArchBox → Machine. Together they are the data of a symmetric monoidal functor C_arch → Machine.

-- Lift a per-channel assignment to a Channel over the whole object term.
objChannels : (ArchChan → Ch.Channel) → ObjTerm → Ch.Channel
objChannels f []       = Ch.I
objChannels f (x ∷ xs) = f x Ch.⊗₀ objChannels f xs
 
unitorˡ : ∀ {X} → Mc.Machine (Ch.I Ch.⊗₀ X) X
unitorˡ = Mc.TotalFunctionMachine' Ch.⊗-left-neutral Ch.⊗-left-intro
 
unitorˡ⁻¹ : ∀ {X} → Mc.Machine X (Ch.I Ch.⊗₀ X)
unitorˡ⁻¹ = Mc.TotalFunctionMachine' Ch.⊗-left-intro Ch.⊗-left-neutral
 
module _ (f : ArchChan → Ch.Channel) where
  mergeᴹ : ∀ A B → Mc.Machine (objChannels f A Ch.⊗₀ objChannels f B) (objChannels f (A ++ B))
  mergeᴹ []       B = unitorˡ
  mergeᴹ (x ∷ xs) B = (f x Mc.⊗ˡ mergeᴹ xs B) Mc.∘ Mc.⊗-assoc
 
  splitᴹ : ∀ A B → Mc.Machine (objChannels f (A ++ B)) (objChannels f A Ch.⊗₀ objChannels f B)
  splitᴹ []       B = unitorˡ⁻¹
  splitᴹ (x ∷ xs) B = Mc.⊗-assoc⃖ Mc.∘ (f x Mc.⊗ˡ splitᴹ xs B)
 
record ChannelModel : Set₁ where
  field
    ⟦TBD⟧            : Ch.Channel
    ⟦TBD-SYNC⟧       : Ch.Channel
    ⟦RECOVERY-P5⟧    : Ch.Channel
    ⟦READ-STATE⟧     : Ch.Channel
    ⟦JUBJUB-SCHNORR⟧ : Ch.Channel
    ⟦STATE⟧          : Ch.Channel
    ⟦WITNESS-IPC⟧    : Ch.Channel
    ⟦CHAIN⟧          : Ch.Channel
    ⟦User⟧           : Ch.Channel
 
  channelSemantics : ArchChan → Ch.Channel
  channelSemantics TBD            = ⟦TBD⟧
  channelSemantics TBD-SYNC       = ⟦TBD-SYNC⟧
  channelSemantics RECOVERY-P5    = ⟦RECOVERY-P5⟧
  channelSemantics READ-STATE     = ⟦READ-STATE⟧
  channelSemantics JUBJUB-SCHNORR = ⟦JUBJUB-SCHNORR⟧
  channelSemantics STATE          = ⟦STATE⟧
  channelSemantics WITNESS-IPC    = ⟦WITNESS-IPC⟧
  channelSemantics CHAIN          = ⟦CHAIN⟧
  channelSemantics User           = ⟦User⟧
 
  -- the functor's action on objects
  ⟦_⟧₀ : ObjTerm → Ch.Channel
  ⟦_⟧₀ = objChannels channelSemantics
 
record MachineModel (channels : ChannelModel) : Set₁ where
  open ChannelModel channels public
  field
    ⟦didContract⟧     : Mc.Machine ⟦ unit ⟧₀ ⟦ Var TBD ⟧₀
    ⟦nameService⟧     : Mc.Machine ⟦ unit ⟧₀ ⟦ Var TBD ⟧₀
    ⟦peerDevices⟧     : Mc.Machine ⟦ unit ⟧₀ ⟦ Var TBD-SYNC ⟧₀
    ⟦recoveryHelpers⟧ : Mc.Machine ⟦ unit ⟧₀ ⟦ Var RECOVERY-P5 ⟧₀
    ⟦indexer⟧         : Mc.Machine ⟦ unit ⟧₀ ⟦ Var READ-STATE ⟧₀
    ⟦accountCustody⟧  : Mc.Machine ⟦ Var TBD ⊗₀ Var TBD ⊗₀ Var CHAIN ⟧₀ ⟦ Var JUBJUB-SCHNORR ⟧₀
    ⟦localWallet⟧     : Mc.Machine ⟦ Var TBD-SYNC ⟧₀ ⟦ Var STATE ⟧₀
    ⟦proofServer⟧     : Mc.Machine ⟦ unit ⟧₀ ⟦ Var WITNESS-IPC ⟧₀
    ⟦passportKey⟧     : Mc.Machine
                          ⟦ Var RECOVERY-P5 ⊗₀ Var READ-STATE ⊗₀ Var JUBJUB-SCHNORR
                          ⊗₀ Var STATE ⊗₀ Var WITNESS-IPC ⟧₀
                          ⟦ Var User ⟧₀
 
  -- The functor from the box generators into the category of machines,
  -- reading each box off its field.
  ⟦_⟧₁ : ∀ {A B} → ArchBox A B → Mc.Machine ⟦ A ⟧₀ ⟦ B ⟧₀
  ⟦ didContract     ⟧₁ = ⟦didContract⟧
  ⟦ nameService     ⟧₁ = ⟦nameService⟧
  ⟦ peerDevices     ⟧₁ = ⟦peerDevices⟧
  ⟦ recoveryHelpers ⟧₁ = ⟦recoveryHelpers⟧
  ⟦ indexer         ⟧₁ = ⟦indexer⟧
  ⟦ accountCustody  ⟧₁ = ⟦accountCustody⟧
  ⟦ localWallet     ⟧₁ = ⟦localWallet⟧
  ⟦ proofServer     ⟧₁ = ⟦proofServer⟧
  ⟦ passportKey     ⟧₁ = ⟦passportKey⟧
 
  -- The induced monoidal functor `C_arch → Machine`
  ⟦_⟧ : ∀ {A B} → WTerm A B → Mc.Machine ⟦ A ⟧₀ ⟦ B ⟧₀
  ⟦ boxʷ b ⟧  = ⟦ b ⟧₁
  ⟦ idʷ ⟧     = Mc.id
  ⟦ g ∘ʷ f ⟧  = ⟦ g ⟧ Mc.∘ ⟦ f ⟧
  ⟦ _⊗ʷ_ {nl} {ml} {nr} {mr} f g ⟧ =
    mergeᴹ channelSemantics ml mr Mc.∘ (⟦ f ⟧ Mc.⊗₁ ⟦ g ⟧) Mc.∘ splitᴹ channelSemantics nl nr
 
  ⟦architecture⟧ : Mc.Machine ⟦ Var CHAIN ⟧₀ ⟦ Var User ⟧₀
  ⟦architecture⟧ = ⟦ architectureᶜ ⟧