module Runtime.Protocol import Runtime.RegionTransfer import Std.Natural import Std.List -- Decision selectors have their own type: a learning operation or payload -- cannot accidentally stand in for a branch predicate. Unconditional protocols -- use this uninhabited type, so no unavailable selector is replaced by a value. family ProtocolNoDecision : Type 0 end-family -- Routes form an ordered dissemination tree after admission. The sender must -- already know the decision, and each receiver is introduced exactly once. -- This represents declared edges, not every member of the execution fleet. family ProtocolAnnouncements : Type 0 parameter erased announcementPayload : Type 0 constructor ProtocolAnnouncementsEnd constructor ProtocolAnnouncementsNext field unrestricted announcementIdentity : (family RegionTransferIdentity) field unrestricted announcementBinding : announcementPayload recursive unrestricted announcementRest end-family -- The global syntax describes dependency order, independent of a device or -- learning algorithm. Repeated and conditional bodies remain shared syntax. family GlobalProtocol : Type 0 parameter erased protocolOperation : Type 0 parameter erased protocolPayload : Type 0 parameter erased protocolDecision : Type 0 constructor GlobalProtocolEnd constructor GlobalProtocolLocal field unrestricted globalLocalParticipant : Nat field unrestricted globalLocalOperation : protocolOperation recursive unrestricted globalLocalRest constructor GlobalProtocolTransfer field unrestricted globalTransferIdentity : (family RegionTransferIdentity) field unrestricted globalTransferPayload : protocolPayload recursive unrestricted globalTransferRest constructor GlobalProtocolRepeat field unrestricted globalRepeatCount : Nat recursive unrestricted globalRepeatBody recursive unrestricted globalRepeatRest constructor GlobalProtocolChoice field unrestricted globalChoiceIdentity : (family RegionTransferIdentity) field unrestricted globalChoiceSelector : protocolDecision field unrestricted globalChoiceAnnouncements : (family ProtocolAnnouncements protocolPayload) recursive unrestricted globalChoiceZero recursive unrestricted globalChoiceOne recursive unrestricted globalChoiceRest end-family family ProtocolDirection : Type 0 constructor ProtocolSend constructor ProtocolReceive end-family family ParticipantProtocol : Type 0 parameter erased participantOperation : Type 0 parameter erased participantPayload : Type 0 parameter erased participantDecision : Type 0 constructor ParticipantProtocolEnd constructor ParticipantProtocolLocal field unrestricted participantLocalOperation : participantOperation recursive unrestricted participantLocalRest constructor ParticipantProtocolTransfer field unrestricted participantTransferDirection : (family ProtocolDirection) field unrestricted participantTransferIdentity : (family RegionTransferIdentity) field unrestricted participantTransferPayload : participantPayload recursive unrestricted participantTransferRest constructor ParticipantProtocolRepeat field unrestricted participantRepeatCount : Nat recursive unrestricted participantRepeatBody recursive unrestricted participantRepeatRest constructor ParticipantProtocolChoice field unrestricted participantChoiceRole : Nat field unrestricted participantChoiceIdentity : (family RegionTransferIdentity) field unrestricted participantChoiceSelector : participantDecision field unrestricted participantChoiceAnnouncements : (family ProtocolAnnouncements participantPayload) recursive unrestricted participantChoiceZero recursive unrestricted participantChoiceOne recursive unrestricted participantChoiceRest end-family family ProtocolFailure : Type 0 constructor ProtocolMembershipBounds constructor ProtocolParticipantBounds constructor ProtocolSenderBounds constructor ProtocolReceiverBounds constructor ProtocolSelfTransfer constructor ProtocolRepeatBounds constructor ProtocolLocalUnavailable constructor ProtocolTransferUnavailable constructor ProtocolChoiceAuthority constructor ProtocolChoiceRoutes constructor ProtocolChoiceUninformed constructor ProtocolChoiceUnavailable end-family def protocolNoDecision = (lambda erased payload : Type 0 . (lambda unrestricted owner : Nat . (lambda unrestricted selector : (family ProtocolNoDecision) . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (eliminate ProtocolNoDecision (lambda unrestricted current : (family ProtocolNoDecision) . Nat) selector))))) def participantProtocolEmpty = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted program : (family ParticipantProtocol operation payload decision) . (eliminate ParticipantProtocol (lambda unrestricted current : (family ParticipantProtocol operation payload decision) . Nat) program (branch ParticipantProtocolEnd . 1) (branch ParticipantProtocolLocal value rest induction . 0) (branch ParticipantProtocolTransfer direction identity value rest induction . 0) (branch ParticipantProtocolRepeat count body rest bodyInduction restInduction . 0) (branch ParticipantProtocolChoice role identity selector announcements zeroBody oneBody rest zeroInduction oneInduction restInduction . 0)))))) def protocolAnnouncementsEmpty = (lambda erased payload : Type 0 . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat) announcements (branch ProtocolAnnouncementsEnd . 1) (branch ProtocolAnnouncementsNext identity value rest induction . 0)))) -- The authority is encoded once, in the canonical choice identity. That -- anchor names the owner in both route fields; real announcements substitute -- their own sender/receiver while preserving every other identity component. def protocolInformed = (lambda erased payload : Type 0 . (lambda unrestricted anchor : (family RegionTransferIdentity) . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (lambda unrestricted role : Nat . (naturalOr (naturalEqual role (regionTransferSender anchor)) (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat) announcements (branch ProtocolAnnouncementsEnd . 0) (branch ProtocolAnnouncementsNext identity value rest induction . (naturalOr (naturalEqual role (regionTransferReceiver identity)) induction)))))))) def projectProtocolAnnouncements = (lambda erased payload : Type 0 . (lambda unrestricted role : Nat . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . (family ProtocolAnnouncements payload)) announcements (branch ProtocolAnnouncementsEnd . (constructor ProtocolAnnouncements ProtocolAnnouncementsEnd payload)) (branch ProtocolAnnouncementsNext identity value rest induction . (nat-eliminate (lambda unrestricted flag : Nat . (family ProtocolAnnouncements payload)) induction (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ProtocolAnnouncements payload) . (constructor ProtocolAnnouncements ProtocolAnnouncementsNext payload identity value induction))) (naturalOr (naturalEqual role (regionTransferSender identity)) (naturalEqual role (regionTransferReceiver identity))))))))) def protocolLocal = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted owner : Nat . (lambda unrestricted value : operation . (lambda unrestricted rest : (family GlobalProtocol operation payload decision) . (constructor GlobalProtocol GlobalProtocolLocal operation payload decision owner value rest))))))) def protocolTransfer = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted value : payload . (lambda unrestricted rest : (family GlobalProtocol operation payload decision) . (constructor GlobalProtocol GlobalProtocolTransfer operation payload decision identity value rest))))))) def protocolRepeat = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted count : Nat . (lambda unrestricted body : (family GlobalProtocol operation payload decision) . (lambda unrestricted rest : (family GlobalProtocol operation payload decision) . (constructor GlobalProtocol GlobalProtocolRepeat operation payload decision count body rest))))))) def protocolChoice = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted selector : decision . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (lambda unrestricted zeroBody : (family GlobalProtocol operation payload decision) . (lambda unrestricted oneBody : (family GlobalProtocol operation payload decision) . (lambda unrestricted rest : (family GlobalProtocol operation payload decision) . (constructor GlobalProtocol GlobalProtocolChoice operation payload decision identity selector announcements zeroBody oneBody rest)))))))))) -- Lift reusable local semantics into a system operation type. Transfers, -- choices and repetition retain their identities and order unchanged. def mapGlobalProtocolOperations = (lambda erased source : Type 0 . (lambda erased target : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted transform : (pi unrestricted value : source . target) . (lambda unrestricted program : (family GlobalProtocol source payload decision) . (eliminate GlobalProtocol (lambda unrestricted current : (family GlobalProtocol source payload decision) . (family GlobalProtocol target payload decision)) program (branch GlobalProtocolEnd . (constructor GlobalProtocol GlobalProtocolEnd target payload decision)) (branch GlobalProtocolLocal role value rest induction . (constructor GlobalProtocol GlobalProtocolLocal target payload decision role (transform value) induction)) (branch GlobalProtocolTransfer identity value rest induction . (constructor GlobalProtocol GlobalProtocolTransfer target payload decision identity value induction)) (branch GlobalProtocolRepeat count body rest bodyResult restResult . (constructor GlobalProtocol GlobalProtocolRepeat target payload decision count bodyResult restResult)) (branch GlobalProtocolChoice identity selector announcements zeroBody oneBody rest zeroResult oneResult restResult . (constructor GlobalProtocol GlobalProtocolChoice target payload decision identity selector announcements zeroResult oneResult restResult))))))))) -- Declared transfer storage occurrences, for local allocation/setup. Repeats -- contribute their body once; both choice arms remain visible. This does not -- report runtime completions or authorize rearming an unselected transfer. def participantProtocolPayloads = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted program : (family ParticipantProtocol operation payload decision) . (eliminate ParticipantProtocol (lambda unrestricted current : (family ParticipantProtocol operation payload decision) . (family StdList payload)) program (branch ParticipantProtocolEnd . (constructor StdList StdListEmpty payload)) (branch ParticipantProtocolLocal value rest induction . induction) (branch ParticipantProtocolTransfer direction identity value rest induction . (constructor StdList StdListCons payload value induction)) (branch ParticipantProtocolRepeat count body rest bodyResult restResult . (stdListAppend payload bodyResult restResult)) (branch ParticipantProtocolChoice role identity selector announcements zeroBody oneBody rest zeroResult oneResult restResult . (stdListAppend payload (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . (family StdList payload)) announcements (branch ProtocolAnnouncementsEnd . (constructor StdList StdListEmpty payload)) (branch ProtocolAnnouncementsNext identity value rest induction . (constructor StdList StdListCons payload value induction))) (stdListAppend payload zeroResult (stdListAppend payload oneResult restResult))))))))) -- Append once at the outer continuation. Repeated/conditional bodies keep -- their original ends; appending there would duplicate the continuation. def appendGlobalProtocol = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted program : (family GlobalProtocol operation payload decision) . (lambda unrestricted tail : (family GlobalProtocol operation payload decision) . (eliminate GlobalProtocol (lambda unrestricted current : (family GlobalProtocol operation payload decision) . (family GlobalProtocol operation payload decision)) program (branch GlobalProtocolEnd . tail) (branch GlobalProtocolLocal role value rest induction . (constructor GlobalProtocol GlobalProtocolLocal operation payload decision role value induction)) (branch GlobalProtocolTransfer identity value rest induction . (constructor GlobalProtocol GlobalProtocolTransfer operation payload decision identity value induction)) (branch GlobalProtocolRepeat count body rest bodyResult restResult . (constructor GlobalProtocol GlobalProtocolRepeat operation payload decision count body restResult)) (branch GlobalProtocolChoice identity selector announcements zeroBody oneBody rest zeroResult oneResult restResult . (constructor GlobalProtocol GlobalProtocolChoice operation payload decision identity selector announcements zeroBody oneBody restResult))))))))