module arch.node.engines.router_messages; import arch.node.engines.net_registry_messages open; import arch.node.types.transport open; import arch.node.types.basics open; import arch.node.types.identities open; import arch.node.types.messages open; type NodeOutMsg M := mkNodeOutMsg@{ prefs : TransportPrefs; expiry : Time; msg : EngineMsg M; }; type NodeMsg := mkNodeMsg@{ seq : Nat; msg : EncryptedMsg; }; type ConnectRequest := mkConnectRequest@{ proto_ver_min : Nat; proto_ver_max : Nat; src_node_id : NodeID; dst_node_id : NodeID; src_node_advert_ver : Nat; dst_node_advert_ver : Nat; }; type ConnectReplyOk := mkConnectReplyOk@{ proto_ver : Nat; node_advert_ver : Pair Nat Nat; }; type ConnectReplyError := | ConnectReplyErrorOverCapacity | ConnectReplyErrorIncompatible | ConnectReplyErrorDenied; ConnectReply : Type := Result ConnectReplyOk ConnectReplyError; type ConnectionPermanence := | RouterMsgConnectionEphemeral | RouterMsgConnectionPermanent; type RouterMsg M := | RouterNodeAdvert NodeAdvert | RouterMsgSend (NodeOutMsg M) | RouterMsgRecv NodeMsg | RouterMsgConnectRequest ConnectRequest | RouterMsgConnectReply ConnectReply | RouterMsgSetPermanence ConnectionPermanence;