module Runtime.NativeProtocol import Runtime.Protocol import Runtime.RegionTransfer import Runtime.RegionFrame import Compiler.Planning.RegionFrame import Runtime.NativeBranch import Runtime.NativeRegionFrame import Runtime.NativeMemoryPlan import Runtime.NativePhysicalProgram import Runtime.NativeLaunchRecipeLoad import Std.Foundation import Std.Natural -- The predicate and its scratch word are separate from frame storage. Only -- the authority evaluates the selector. Followers install the validated wire -- word, and forwarding participants publish that exact installed value. family NativeProtocolDecisionBinding : Type 0 parameter erased nativeDecisionSelector : Type 0 parameter erased nativeDecisionPayload : Type 0 constructor NativeProtocolDecisionBindingOf field unrestricted nativeDecisionSource : (pi unrestricted selector : nativeDecisionSelector . (family NativePhysicalOperand)) field unrestricted nativeDecisionState : (pi unrestricted selector : nativeDecisionSelector . Nat) field unrestricted nativeDecisionScratchSlot : Nat field unrestricted nativeDecisionFrame : (pi unrestricted value : nativeDecisionPayload . (family RegionFrameLayout)) end-family -- A transfer binding must reproduce the canonical route, identity and extent -- from the global protocol. A matching local buffer size alone is insufficient. def nativeProtocolFrameAdmitted = (lambda unrestricted identity : (family RegionTransferIdentity) . (lambda unrestricted layout : (family RegionFrameLayout) . (eliminate StdResult (lambda unrestricted result : (family StdResult (family RegionFrameFailure) Bytes) . Nat) (regionFrameHeader identity (framePayloadBytes layout) (bytes-length (frameHeader layout))) (branch StdFailure error . 0) (branch StdSuccess header . (bytes-equal header (frameHeader layout)))))) def nativeProtocolDecisionSource = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (eliminate NativeProtocolDecisionBinding (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) . (pi unrestricted selector : decision . (family NativePhysicalOperand))) binding (branch NativeProtocolDecisionBindingOf source state scratch frame . source))))) def nativeProtocolDecisionState = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (eliminate NativeProtocolDecisionBinding (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) . (pi unrestricted selector : decision . Nat)) binding (branch NativeProtocolDecisionBindingOf source state scratch frame . state))))) def nativeProtocolDecisionScratch = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (eliminate NativeProtocolDecisionBinding (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) . Nat) binding (branch NativeProtocolDecisionBindingOf source state scratch frame . scratch))))) def nativeProtocolDecisionFrame = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (eliminate NativeProtocolDecisionBinding (lambda unrestricted current : (family NativeProtocolDecisionBinding decision payload) . (pi unrestricted value : payload . (family RegionFrameLayout))) binding (branch NativeProtocolDecisionBindingOf source state scratch frame . frame))))) def nativeProtocolNoFrameDecisions = (constructor NativeProtocolDecisionBinding NativeProtocolDecisionBindingOf (family ProtocolNoDecision) (family RegionFrameLayout) (lambda unrestricted selector : (family ProtocolNoDecision) . (eliminate ProtocolNoDecision (lambda unrestricted current : (family ProtocolNoDecision) . (family NativePhysicalOperand)) selector)) (lambda unrestricted selector : (family ProtocolNoDecision) . (eliminate ProtocolNoDecision (lambda unrestricted current : (family ProtocolNoDecision) . Nat) selector)) 0 (lambda unrestricted frame : (family RegionFrameLayout) . frame)) -- The choice payload is a single canonical word. Admission checks every -- declared announcement binding before either participant artifact is emitted. -- The decision word must be disjoint from frame storage: framing/hash work may -- overwrite its scratch/header bytes while an authority is still forwarding. -- The complete host arena and result-slot capacities remain outer admission facts. def nativeProtocolDecisionAdmitted = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (lambda unrestricted owner : Nat . (lambda unrestricted selector : decision . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (let unrestricted state = (nativeProtocolDecisionState decision payload binding selector) in (let unrestricted wordBytes = (bytes-length (regionFrameWord 0)) in (naturalAnd (naturalLessOrEqual state (naturalSaturatingSubtract regionFrameWordLimit wordBytes)) (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat) announcements (branch ProtocolAnnouncementsEnd . 1) (branch ProtocolAnnouncementsNext identity value rest induction . (let unrestricted frame = (nativeProtocolDecisionFrame decision payload binding value) in (naturalAnd (nativeProtocolFrameAdmitted identity frame) (naturalAnd (naturalEqual (framePayloadBytes frame) wordBytes) (naturalAnd (naturalOr (naturalLessOrEqual (naturalAdd state wordBytes) (frameBase frame)) (naturalLessOrEqual (frameEnd frame) state)) (naturalAnd induction 1)))))))))))))))) def nativeProtocolRequireDecision = (lambda unrestricted value : (family NativePhysicalOperand) . (lambda unrestricted label : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalAssertOneOf value (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 1) (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed)) label tail)))) -- A received frame is consumed before its value can control local work. A -- forwarder reuses that installed value, never its own selector. Each edge -- advances its own invocation version, so repeats and nested choices retain -- replay protection without introducing another native repeat frame. def nativeProtocolAnnouncements = (lambda erased decision : Type 0 . (lambda erased payload : Type 0 . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (lambda unrestricted selector : decision . (lambda unrestricted role : Nat . (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) . (lambda unrestricted label : Bytes . (lambda unrestricted announcements : (family ProtocolAnnouncements payload) . (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) announcements (branch ProtocolAnnouncementsEnd . (lambda unrestricted tail : (family NativePhysicalCommands) . tail)) (branch ProtocolAnnouncementsNext identity value rest induction . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted frame = (nativeProtocolDecisionFrame decision payload binding value) in (let unrestricted state = (nativeProtocolDecisionState decision payload binding selector) in (nat-eliminate (lambda unrestricted flag : Nat . (family NativePhysicalCommands)) (transfer (constructor ProtocolDirection ProtocolReceive) identity value (nativeFrameConsume frame (nativeMemoryStoreWord64 label state (nativeMemoryLoad (framePayloadAt frame)) (nativeProtocolRequireDecision (nativeMemoryLoad state) label (nativeFrameAdvance frame (constructor NativeFrameTerminal NativeFrameConsumeComplete) (nativeProtocolDecisionScratch decision payload binding) (induction tail)))))) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeMemoryStoreWord64 label (framePayloadAt frame) (nativeMemoryLoad state) (transfer (constructor ProtocolDirection ProtocolSend) identity value (nativeFrameAdvance frame (constructor NativeFrameTerminal NativeFrameSendComplete) (nativeProtocolDecisionScratch decision payload binding) (induction tail)))))) (naturalEqual role (regionTransferSender identity)))))))))))))))) -- Lower admitted projections only. Callbacks may realize local computation or -- declared transfers but cannot introduce hidden network dependencies. The -- selector is evaluated once by the authority before any outgoing announcement. -- Native repeat admission remains the shared encoder's responsibility. def nativeProtocolCommands = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted local : (pi unrestricted value : operation . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) . (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) . (lambda unrestricted binding : (family NativeProtocolDecisionBinding decision payload) . (lambda unrestricted label : Bytes . (lambda unrestricted program : (family ParticipantProtocol operation payload decision) . (eliminate ParticipantProtocol (lambda unrestricted current : (family ParticipantProtocol operation payload decision) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) program (branch ParticipantProtocolEnd . (lambda unrestricted tail : (family NativePhysicalCommands) . tail)) (branch ParticipantProtocolLocal value rest induction . (lambda unrestricted tail : (family NativePhysicalCommands) . (local value (induction tail)))) (branch ParticipantProtocolTransfer direction identity value rest induction . (lambda unrestricted tail : (family NativePhysicalCommands) . (transfer direction identity value (induction tail)))) (branch ParticipantProtocolRepeat count body rest bodyLowering restLowering . (lambda unrestricted tail : (family NativePhysicalCommands) . (nat-eliminate (lambda unrestricted flag : Nat . (family NativePhysicalCommands)) (restLowering tail) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeImmediate count)) (bytes-append label b":begin") (bodyLowering (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) (bytes-append label b":end") (restLowering tail)))))) count))) (branch ParticipantProtocolChoice role identity selector announcements zeroBody oneBody rest zeroLowering oneLowering restLowering . (lambda unrestricted tail : (family NativePhysicalCommands) . (let unrestricted state = (nativeProtocolDecisionState decision payload binding selector) in (let unrestricted selected = (nativeProtocolAnnouncements decision payload binding selector role transfer label announcements (nativeIfEqual (nativeMemoryLoad state) (nativeLaunchRecipeImmediate 0) label (zeroLowering (constructor NativePhysicalCommands NativePhysicalCommandsEnd)) (oneLowering (constructor NativePhysicalCommands NativePhysicalCommandsEnd)) (restLowering tail))) in (nat-eliminate (lambda unrestricted flag : Nat . (family NativePhysicalCommands)) selected (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family NativePhysicalCommands) . (nativeMemoryStoreWord64 label state (nativeProtocolDecisionSource decision payload binding selector) (nativeProtocolRequireDecision (nativeMemoryLoad state) label selected)))) (naturalEqual role (regionTransferSender identity)))))))))))))))) -- Setup traverses every declared frame once per occurrence, without executing -- choices or repeat counts. The callback is for setup, not runtime advancement: -- an unselected branch has no completed transfer to rearm. Reinitializing an -- already live frame through this traversal is forbidden by the frame contract. def nativeProtocolFrames = (lambda erased operation : Type 0 . (lambda erased payload : Type 0 . (lambda erased decision : Type 0 . (lambda unrestricted transfer : (pi unrestricted direction : (family ProtocolDirection) . (pi unrestricted identity : (family RegionTransferIdentity) . (pi unrestricted value : payload . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))) . (lambda unrestricted program : (family ParticipantProtocol operation payload decision) . (eliminate ParticipantProtocol (lambda unrestricted current : (family ParticipantProtocol operation payload decision) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) program (branch ParticipantProtocolEnd . (lambda unrestricted tail : (family NativePhysicalCommands) . tail)) (branch ParticipantProtocolLocal value rest induction . induction) (branch ParticipantProtocolTransfer direction identity value rest induction . (lambda unrestricted tail : (family NativePhysicalCommands) . (transfer direction identity value (induction tail)))) (branch ParticipantProtocolRepeat count body rest bodyFrames restFrames . (lambda unrestricted tail : (family NativePhysicalCommands) . (bodyFrames (restFrames tail)))) (branch ParticipantProtocolChoice role identity selector announcements zeroBody oneBody rest zeroFrames oneFrames restFrames . (lambda unrestricted tail : (family NativePhysicalCommands) . (app (eliminate ProtocolAnnouncements (lambda unrestricted current : (family ProtocolAnnouncements payload) . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))) announcements (branch ProtocolAnnouncementsEnd . (lambda unrestricted tail : (family NativePhysicalCommands) . tail)) (branch ProtocolAnnouncementsNext identity value rest induction . (lambda unrestricted tail : (family NativePhysicalCommands) . (transfer (nat-eliminate (lambda unrestricted flag : Nat . (family ProtocolDirection)) (constructor ProtocolDirection ProtocolReceive) (lambda unrestricted prior : Nat . (lambda unrestricted ignored : (family ProtocolDirection) . (constructor ProtocolDirection ProtocolSend))) (naturalEqual role (regionTransferSender identity))) identity value (induction tail))))) (zeroFrames (oneFrames (restFrames tail))))))))))))