module Compiler.Planning.Protocol import Runtime.Protocol import Runtime.RegionTransfer import Runtime.RegionFrame import Std.Foundation import Std.Natural -- Every admission check precedes local program emission. A backend supplies -- capability checks for its typed operations and transfer bindings; an absent -- lowering is a refusal, never an empty command or a host substitution. def protocolAccepted : (family StdResult (family ProtocolFailure) Nat) = (constructor StdResult StdSuccess (family ProtocolFailure) Nat 1) def protocolRequire = (lambda unrestricted flag : Nat . (lambda unrestricted failure : (family ProtocolFailure) . (lambda unrestricted next : (family StdResult (family ProtocolFailure) Nat) . (nat-eliminate (lambda unrestricted current : Nat . (family StdResult (family ProtocolFailure) Nat)) (constructor StdResult StdFailure (family ProtocolFailure) Nat failure) (lambda unrestricted previous : Nat . (lambda unrestricted ignored : (family StdResult (family ProtocolFailure) Nat) . next)) flag)))) def protocolCheckThen = (lambda unrestricted first : (family StdResult (family ProtocolFailure) Nat) . (lambda unrestricted next : (family StdResult (family ProtocolFailure) Nat) . (eliminate StdResult (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) . (family StdResult (family ProtocolFailure) Nat)) first (branch StdFailure error . (constructor StdResult StdFailure (family ProtocolFailure) Nat error)) (branch StdSuccess value . next)))) -- A topologically ordered tree has one authority and one incoming decision -- per receiver. Admission checks the declared edges only. The current source -- implementation uses a persistent membership predicate (quadratic in edges -- in the worst case); hierarchical fleet planning must bound per-cell edges. def protocolAnnouncementsAdmitted = (lambda erased payload : Type 0 . (lambda unrestricted participants : Nat . (lambda unrestricted anchor : (family RegionTransferIdentity) . (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (app (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . (pi unrestricted known : (pi unrestricted role : Nat . Nat) . Nat)) announcements (branch ProtocolAnnouncementsEnd . (lambda unrestricted known : (pi unrestricted role : Nat . Nat) . 1)) (branch ProtocolAnnouncementsNext identity value rest induction . (lambda unrestricted known : (pi unrestricted role : Nat . Nat) . (naturalAnd (known (regionTransferSender identity)) (naturalAnd (naturalEqual (known (regionTransferReceiver identity)) 0) (naturalAnd (naturalLess (regionTransferReceiver identity) participants) (naturalAnd (regionTransferIdentityEqual (regionTransferWithRoute anchor (regionTransferSender identity) (regionTransferReceiver identity)) identity) (naturalAnd (transfer identity value) (naturalAnd (induction (lambda unrestricted role : Nat . (naturalOr (known role) (naturalEqual role (regionTransferReceiver identity))))) 1))))))))) (lambda unrestricted role : Nat . (naturalEqual role (regionTransferSender anchor))))))))) -- Every participant mentioned in either conditional body must know the -- decision, including forwarding-only roles of a nested choice. No guessing -- or implicit merging of unrelated branch schedules is permitted. def globalProtocolCovered = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted known : (pi unrestricted role : Nat . Nat) . (lambda unrestricted program : (family GlobalProtocol operation payload decision) . (eliminate GlobalProtocol (lambda unrestricted current : (family GlobalProtocol operation payload decision) . Nat) program (branch GlobalProtocolEnd . 1) (branch GlobalProtocolLocal role value rest induction . (naturalAnd (known role) induction)) (branch GlobalProtocolTransfer identity value rest induction . (naturalAnd (known (regionTransferSender identity)) (naturalAnd (known (regionTransferReceiver identity)) (naturalAnd induction 1)))) (branch GlobalProtocolRepeat count body rest bodyCheck restCheck . (naturalAnd bodyCheck restCheck)) (branch GlobalProtocolChoice identity selector announcements zeroBody oneBody rest zeroCheck oneCheck restCheck . (naturalAnd (known (regionTransferSender identity)) (naturalAnd (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat) announcements (branch ProtocolAnnouncementsEnd . 1) (branch ProtocolAnnouncementsNext edge value tail induction . (naturalAnd (known (regionTransferSender edge)) (naturalAnd (known (regionTransferReceiver edge)) (naturalAnd induction 1))))) (naturalAnd zeroCheck (naturalAnd oneCheck (naturalAnd restCheck 1)))))))))))) def checkGlobalProtocol = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted participants : Nat . (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) . (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) . (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) . (lambda unrestricted program : (family GlobalProtocol operation payload decision) . (protocolRequire (naturalAnd (naturalNonzero participants) (naturalLessOrEqual participants regionFrameWordLimit)) (constructor ProtocolFailure ProtocolMembershipBounds) (eliminate GlobalProtocol (lambda unrestricted current : (family GlobalProtocol operation payload decision) . (family StdResult (family ProtocolFailure) Nat)) program (branch GlobalProtocolEnd . protocolAccepted) (branch GlobalProtocolLocal participant value rest induction . (protocolRequire (naturalLess participant participants) (constructor ProtocolFailure ProtocolParticipantBounds) (protocolRequire (local participant value) (constructor ProtocolFailure ProtocolLocalUnavailable) induction))) (branch GlobalProtocolTransfer identity value rest induction . (protocolRequire (naturalLess (regionTransferSender identity) participants) (constructor ProtocolFailure ProtocolSenderBounds) (protocolRequire (naturalLess (regionTransferReceiver identity) participants) (constructor ProtocolFailure ProtocolReceiverBounds) (protocolRequire (naturalEqual (naturalEqual (regionTransferSender identity) (regionTransferReceiver identity)) 0) (constructor ProtocolFailure ProtocolSelfTransfer) (protocolRequire (transfer identity value) (constructor ProtocolFailure ProtocolTransferUnavailable) induction))))) (branch GlobalProtocolRepeat count body rest bodyCheck restCheck . (protocolRequire (naturalLessOrEqual count regionFrameWordLimit) (constructor ProtocolFailure ProtocolRepeatBounds) (protocolCheckThen bodyCheck (protocolCheckThen restCheck protocolAccepted)))) (branch GlobalProtocolChoice identity selector announcements zeroBody oneBody rest zeroCheck oneCheck restCheck . (protocolRequire (naturalAnd (naturalLess (regionTransferSender identity) participants) (naturalEqual (regionTransferSender identity) (regionTransferReceiver identity))) (constructor ProtocolFailure ProtocolChoiceAuthority) (protocolRequire (protocolAnnouncementsAdmitted payload participants identity transfer announcements) (constructor ProtocolFailure ProtocolChoiceRoutes) (protocolRequire (naturalAnd (globalProtocolCovered operation payload decision (protocolInformed payload identity announcements) zeroBody) (globalProtocolCovered operation payload decision (protocolInformed payload identity announcements) oneBody)) (constructor ProtocolFailure ProtocolChoiceUninformed) (protocolRequire (choice (regionTransferSender identity) selector announcements) (constructor ProtocolFailure ProtocolChoiceUnavailable) (protocolCheckThen zeroCheck (protocolCheckThen oneCheck (protocolCheckThen restCheck protocolAccepted)))))))))))))))))) -- Projection preserves bodies once, and does not enumerate fleet membership. -- This helper requires admission; planParticipantProtocol is the checked entry. def projectGlobalProtocol = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted participant : Nat . (lambda unrestricted program : (family GlobalProtocol operation payload decision) . (eliminate GlobalProtocol (lambda unrestricted current : (family GlobalProtocol operation payload decision) . (family ParticipantProtocol operation payload decision)) program (branch GlobalProtocolEnd . (constructor ParticipantProtocol ParticipantProtocolEnd operation payload decision)) (branch GlobalProtocolLocal owner value rest induction . (nat-eliminate (lambda unrestricted flag : Nat . (family ParticipantProtocol operation payload decision)) induction (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) . (constructor ParticipantProtocol ParticipantProtocolLocal operation payload decision value induction))) (naturalEqual participant owner))) (branch GlobalProtocolTransfer identity value rest induction . (nat-eliminate (lambda unrestricted flag : Nat . (family ParticipantProtocol operation payload decision)) (nat-eliminate (lambda unrestricted flag : Nat . (family ParticipantProtocol operation payload decision)) induction (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) . (constructor ParticipantProtocol ParticipantProtocolTransfer operation payload decision (constructor ProtocolDirection ProtocolReceive) identity value induction))) (naturalEqual participant (regionTransferReceiver identity))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) . (constructor ParticipantProtocol ParticipantProtocolTransfer operation payload decision (constructor ProtocolDirection ProtocolSend) identity value induction))) (naturalEqual participant (regionTransferSender identity)))) (branch GlobalProtocolRepeat count body rest bodyProjection restProjection . (nat-eliminate (lambda unrestricted flag : Nat . (family ParticipantProtocol operation payload decision)) restProjection (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) . (constructor ParticipantProtocol ParticipantProtocolRepeat operation payload decision count bodyProjection restProjection))) (naturalMultiply count (naturalEqual (participantProtocolEmpty operation payload decision bodyProjection) 0)))) (branch GlobalProtocolChoice identity selector announcements zeroBody oneBody rest zeroProjection oneProjection restProjection . (let unrestricted projectedAnnouncements = (projectProtocolAnnouncements payload participant announcements) in (nat-eliminate (lambda unrestricted flag : Nat . (family ParticipantProtocol operation payload decision)) (constructor ParticipantProtocol ParticipantProtocolChoice operation payload decision participant identity selector projectedAnnouncements zeroProjection oneProjection restProjection) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ParticipantProtocol operation payload decision) . restProjection)) (naturalAnd (protocolAnnouncementsEmpty payload projectedAnnouncements) (naturalAnd (participantProtocolEmpty operation payload decision zeroProjection) (participantProtocolEmpty operation payload decision oneProjection)))))))))))) def planParticipantProtocol = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted participants : Nat . (lambda unrestricted participant : Nat . (lambda unrestricted local : (pi unrestricted owner : Nat . (pi unrestricted value : operation . Nat)) . (lambda unrestricted transfer : (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . Nat)) . (lambda unrestricted choice : (pi unrestricted owner : Nat . (pi unrestricted selector : decision . (pi unrestricted announcements : (family ProtocolAnnouncements payload) . Nat))) . (lambda unrestricted program : (family GlobalProtocol operation payload decision) . (eliminate StdResult (lambda unrestricted current : (family StdResult (family ProtocolFailure) Nat) . (family StdResult (family ProtocolFailure) (family ParticipantProtocol operation payload decision))) (protocolRequire (naturalLess participant participants) (constructor ProtocolFailure ProtocolParticipantBounds) (checkGlobalProtocol operation payload decision participants local transfer choice program)) (branch StdFailure error . (constructor StdResult StdFailure (family ProtocolFailure) (family ParticipantProtocol operation payload decision) error)) (branch StdSuccess accepted . (constructor StdResult StdSuccess (family ProtocolFailure) (family ParticipantProtocol operation payload decision) (projectGlobalProtocol operation payload decision participant program)))))))))))))