module Runtime.NativeTelemetryPolicy import Compiler.MachineX86Native import Compiler.MachineX86NativeAssembly import Data.Bytes import Model.Word64 import Observe.CapturePolicy import Observe.Value import Runtime.NativeLaunchRecipeLoad import Runtime.NativePhysicalProgram import Runtime.NativeTelemetryCapture import Runtime.NativeTelemetryDrain import Runtime.NativeTelemetryIdentity import Std.Byte import Runtime.NativeTelemetryRecord import Runtime.NativeTelemetryPublication import Runtime.NativeTelemetrySeal import Runtime.TelemetryCapture import Runtime.TelemetryDrain import Runtime.TelemetryPolicy import Runtime.TelemetryPolicyRoutine import Runtime.TelemetryPublication import Runtime.TelemetryRecord import Std.Natural import Runtime.NativeWordDigest -- An omitted word is not the number zero. Selected recipes must bind every -- source word they actually reference. Unused binary padding is zeroed without -- reading an application operand, and no tagged observation claims that padding. family NativeTelemetrySourceWord : Type 0 constructor NativeTelemetryWordOmitted constructor NativeTelemetryWordValue field unrestricted nativeTelemetryWordOperand : (family NativePhysicalOperand) end-family family NativeTelemetrySourceValues : Type 0 constructor NativeTelemetrySourceValuesValue field unrestricted nativeTelemetrySourceWord0 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord1 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord2 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord3 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord4 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord5 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord6 : (family NativeTelemetrySourceWord) field unrestricted nativeTelemetrySourceWord7 : (family NativeTelemetrySourceWord) end-family def nativeTelemetrySourceAt = (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted index : Nat . (eliminate NativeTelemetrySourceValues (lambda unrestricted current : (family NativeTelemetrySourceValues) . (family NativeTelemetrySourceWord)) values (branch NativeTelemetrySourceValuesValue word0 word1 word2 word3 word4 word5 word6 word7 . (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 0) word0 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 1) word1 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 2) word2 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 3) word3 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 4) word4 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 5) word5 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 6) word6 (aosChoose (family NativeTelemetrySourceWord) (naturalEqual index 7) word7 (constructor NativeTelemetrySourceWord NativeTelemetryWordOmitted))))))))))))) def nativeTelemetrySourcePresent = (lambda unrestricted source : (family NativeTelemetrySourceWord) . (eliminate NativeTelemetrySourceWord (lambda unrestricted current : (family NativeTelemetrySourceWord) . Nat) source (branch NativeTelemetryWordOmitted . 0) (branch NativeTelemetryWordValue operand . 1))) def nativeTelemetrySourcesAdmission = (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (eliminate TelemetryRecordPlan (lambda unrestricted current : (family TelemetryRecordPlan) . Nat) recipe (branch TelemetryRecordReady parts template . (nat-eliminate (lambda unrestricted count : Nat . Nat) 1 (lambda unrestricted index : Nat . (lambda unrestricted induction : Nat . (naturalAnd induction (naturalOr (naturalIsZero (telemetryRecordWordRequired parts index)) (nativeTelemetrySourcePresent (nativeTelemetrySourceAt values index)))))) captureValueWords)) (branch TelemetryRecordRefused reason . 0)))) def nativeTelemetrySourceOperand = (lambda unrestricted source : (family NativeTelemetrySourceWord) . (eliminate NativeTelemetrySourceWord (lambda unrestricted current : (family NativeTelemetrySourceWord) . (family NativePhysicalOperand)) source (branch NativeTelemetryWordOmitted . (nativeLaunchRecipeImmediate 0)) (branch NativeTelemetryWordValue operand . operand))) -- System V: control, publication state, coordinate, private decision word, -- publication extent, unused. Return one to invoke acquisition (including an -- exclusion), zero on refusal. The private decision is 0/1, or explicit refusal -- 4. Counter and lifetime checks precede source-operand evaluation in the VM. def policyX86SetWord = (lambda unrestricted register : (family X86NativeRegister64) . (lambda unrestricted value : Nat . (digestEmit (constructor X86NativeInstruction X86NativeMoveImmediate64 register (x86NativeImmediate64FromNatural value))))) def policyX86Divide = (lambda unrestricted divisor : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeDivideRegister64Unsigned divisor))) def policyX86Multiply = (lambda unrestricted factor : (family X86NativeRegister64) . (digestEmit (constructor X86NativeInstruction X86NativeMultiplyRegister64Unsigned factor))) def policyX86JumpIf = (lambda unrestricted condition : (family TelemetryPolicyCondition) . (digestJumpIf (eliminate TelemetryPolicyCondition (lambda unrestricted current : (family TelemetryPolicyCondition) . (family X86NativeCondition)) condition (branch TelemetryPolicyZero . (constructor X86NativeCondition X86NativeConditionZero)) (branch TelemetryPolicyNotZero . (constructor X86NativeCondition X86NativeConditionNotZero)) (branch TelemetryPolicyBelow . (constructor X86NativeCondition X86NativeConditionBelow)) (branch TelemetryPolicyAbove . (constructor X86NativeCondition X86NativeConditionAbove))))) def policyX86Backend = (constructor TelemetryPolicyBackend TelemetryPolicyBackendValue (family X86NativeAssembly) (family X86NativeRegister64) digestMovImm policyX86SetWord digestMov digestStore64 digestLoad64 digestCmpImm publicationCompare publicationSubtract digestAdd policyX86Divide policyX86Multiply policyX86JumpIf publicationJump digestLabel digestReturn digestEnd digestRAX digestRDI digestRSI digestRDX digestRCX digestR8 digestR9 digestR10 digestR11) def nativeTelemetrySiteSelectionRoutine = (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted required : Nat . (lambda unrestricted enabled : Nat . (lambda unrestricted stride : Nat . (lambda unrestricted bound : Nat . (compiler-native-encode (family X86NativeAssembly) (telemetryPolicySiteAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) policyX86Backend ordinaryCapacity reservedCapacity required enabled stride bound)))))))) def nativeTelemetryPolicyState = (lambda unrestricted at : Nat . (constructor NativePhysicalOperand NativePhysicalStateAddress (modelWord64FromNaturalTruncated at))) def nativeTelemetryPolicyLoad = (lambda unrestricted at : Nat . (constructor NativePhysicalOperand NativePhysicalStateLoad64 (modelWord64FromNaturalTruncated at))) -- Macro operands may not read outputs this operation overwrites, its -- values/decision scratch, or command-relative payloads that would move to a -- different generated command. Caller-relative affine values are materialized -- from a saved caller iteration instead of a conditional block's iteration. -- Interval tests subtract from the admitted arena boundaries, never add to an -- arbitrary input offset. Even an excluded out-of-range u64 operand must not -- overflow while checking scratch aliasing. The VM owns actual address bounds. def nativeTelemetrySourceScopeAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted operand : (family NativePhysicalOperand) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . Nat) operand (branch NativePhysicalImmediate value . 1) (branch NativePhysicalResultValue slot . (eliminate NativePhysicalSlot (lambda unrestricted current : (family NativePhysicalSlot) . Nat) slot (branch NativePhysicalSlotValue index . (naturalAnd (naturalIsZero (naturalEqual (modelWord64Natural index) resultSlot)) (naturalIsZero (naturalEqual (modelWord64Natural index) workSlot)))))) (branch NativePhysicalResultAddress slot offset . 1) (branch NativePhysicalStateAddress offset . 1) (branch NativePhysicalStateLoad64 offset . (naturalAnd (naturalOr (naturalAnd (naturalLessOrEqual captureWordBytes (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity)) (naturalLessOrEqual (modelWord64Natural offset) (naturalSaturatingSubtract (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity) captureWordBytes))) (naturalLessOrEqual (naturalAdd (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity) captureValuesBytes) (modelWord64Natural offset))) (naturalOr (naturalAnd (naturalLessOrEqual captureWordBytes decisionAt) (naturalLessOrEqual (modelWord64Natural offset) (naturalSaturatingSubtract decisionAt captureWordBytes))) (naturalLessOrEqual (naturalAdd decisionAt (naturalMultiply 2 captureWordBytes)) (modelWord64Natural offset))))) (branch NativePhysicalPayloadAddress offset . 0) (branch NativePhysicalPayloadLoad64 offset . 0) (branch NativePhysicalProcessArgument index . 1) (branch NativePhysicalLoopAffine base stride . 1))))))))) def nativeTelemetrySourceScopesWith = (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted check : (pi unrestricted operand : (family NativePhysicalOperand) . Nat) . (eliminate TelemetryRecordPlan (lambda unrestricted current : (family TelemetryRecordPlan) . Nat) recipe (branch TelemetryRecordReady parts template . (nat-eliminate (lambda unrestricted count : Nat . Nat) 1 (lambda unrestricted index : Nat . (lambda unrestricted induction : Nat . (naturalAnd induction (aosChoose Nat (telemetryRecordWordRequired parts index) (eliminate NativeTelemetrySourceWord (lambda unrestricted current : (family NativeTelemetrySourceWord) . Nat) (nativeTelemetrySourceAt values index) (branch NativeTelemetryWordOmitted . 0) (branch NativeTelemetryWordValue operand . (check operand))) 1)))) captureValueWords)) (branch TelemetryRecordRefused reason . 0))))) def nativeTelemetrySourceScopesAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (nativeTelemetrySourceScopesWith recipe values (nativeTelemetrySourceScopeAdmission applicationBytes ordinaryCapacity reservedCapacity decisionAt resultSlot workSlot)))))))))) def nativeTelemetrySourceAffineRoutine = (compiler-native-encode (family X86NativeAssembly) (telemetryPolicyAffineAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) policyX86Backend)) def nativeTelemetryEmitSource = (lambda unrestricted destination : (family NativePhysicalOperand) . (lambda unrestricted operand : (family NativePhysicalOperand) . (lambda unrestricted iterationAt : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . (family NativePhysicalCommands)) operand (branch NativePhysicalImmediate value . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalResultValue slot . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalResultAddress slot offset . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalStateAddress offset . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalStateLoad64 offset . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalPayloadAddress offset . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalPayloadLoad64 offset . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalProcessArgument index . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 destination operand) identity tail)) (branch NativePhysicalLoopAffine base stride . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetrySourceAffineRoutine (nativeLaunchRecipeArguments (nativeTelemetryPolicyLoad iterationAt) (constructor NativePhysicalOperand NativePhysicalImmediate base) (constructor NativePhysicalOperand NativePhysicalImmediate stride) destination) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))))))) def nativeTelemetryFillSources = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted iterationAt : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryRecordPlan (lambda unrestricted current : (family TelemetryRecordPlan) . (family NativePhysicalCommands)) recipe (branch TelemetryRecordReady parts template . (app (nat-eliminate (lambda unrestricted count : Nat . (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands))) (lambda unrestricted commands : (family NativePhysicalCommands) . commands) (lambda unrestricted index : Nat . (lambda unrestricted induction : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted commands : (family NativePhysicalCommands) . (nativeTelemetryEmitSource (nativeTelemetryPolicyState (naturalAdd (captureValuesScratchAt applicationBytes ordinaryCapacity reservedCapacity) (naturalMultiply index captureWordBytes))) (aosChoose (family NativePhysicalOperand) (telemetryRecordWordRequired parts index) (nativeTelemetrySourceOperand (nativeTelemetrySourceAt values index)) (nativeLaunchRecipeImmediate 0)) iterationAt identity (induction commands))))) captureValueWords) tail)) (branch TelemetryRecordRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail))))))))))) def nativeTelemetryPolicyFillSelected = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted enabled : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (aosChoose (family NativePhysicalCommands) enabled (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeTelemetryPolicyLoad decisionAt)) identity (nativeTelemetryFillSources applicationBytes ordinaryCapacity reservedCapacity recipe values (naturalAdd decisionAt captureWordBytes) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail))) tail)))))))))) def nativeTelemetrySiteWith = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bound : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted capture : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 (nativeTelemetryPolicyState (naturalAdd decisionAt captureWordBytes)) (constructor NativePhysicalOperand NativePhysicalLoopAffine (modelWord64FromNaturalTruncated 0) (modelWord64FromNaturalTruncated 1))) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (nativeTelemetrySiteSelectionRoutine ordinaryCapacity reservedCapacity (capturePolicyRequired policy) (captureSiteSelected policy site) (captureSiteStride site) bound) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeTelemetryPolicyState (captureControlAt applicationBytes)) (nativeTelemetryPolicyState (publicationBase applicationBytes ordinaryCapacity reservedCapacity)) (aosChoose (family NativePhysicalOperand) (naturalAnd (captureSiteSelected policy site) (naturalIsZero (naturalEqual (captureSiteStride site) 1))) coordinate (nativeLaunchRecipeImmediate 0)) (nativeTelemetryPolicyState decisionAt) (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound)) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore workSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine recordStatusRoutine (nativeLaunchRecipeArguments (nativeTelemetryPolicyState decisionAt) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue workSlot)) identity (nativeTelemetryPolicyFillSelected applicationBytes ordinaryCapacity reservedCapacity recipe values (captureSiteSelected policy site) decisionAt identity (capture (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail)))))))))))))))))))))) def nativeTelemetrySiteCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted policy : (family CapturePolicy) . (lambda unrestricted site : (family CaptureSite) . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted recipe : (family TelemetryRecordPlan) . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeTelemetrySiteWith applicationBytes policy site ordinaryCapacity reservedCapacity bound (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) recipe values coordinate resultSlot workSlot identity (nativeTelemetryCaptureSelectedCommand applicationBytes ordinaryCapacity reservedCapacity (nativeTelemetryPolicyLoad (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (captureSiteReserved site) resultSlot identity) tail)))))))))))))))) -- Source operands are evaluated only for selected opportunities. Missing -- required words and scope-changing/aliased inputs refuse build; zero is never -- manufactured for an omitted observation. Padding alone is explicitly zero. def nativeTelemetryCaptureSiteCommand = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryPolicyPlan) . (lambda unrestricted role : Nat . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryPolicyPlan (lambda unrestricted current : (family TelemetryPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryPolicyReady policy ordinarySite reservedSite drain . (eliminate TelemetryDrainPlan (lambda unrestricted current : (family TelemetryDrainPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDrainReady ordinaryCapacity reservedCapacity ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (naturalAnd (naturalLessOrEqual role 1) (naturalAnd (naturalIsZero (naturalEqual resultSlot workSlot)) (naturalAnd (telemetryPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalAnd (naturalOr (naturalIsZero (captureSiteSelected policy (aosChoose (family CaptureSite) role reservedSite ordinarySite))) (naturalAnd (nativeTelemetrySourcesAdmission (aosChoose (family TelemetryRecordPlan) role reserved ordinary) values) (nativeTelemetrySourceScopesAdmission applicationBytes ordinaryCapacity reservedCapacity (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) resultSlot workSlot (aosChoose (family TelemetryRecordPlan) role reserved ordinary) values))) (naturalOr (naturalIsZero (naturalAnd (captureSiteSelected policy (aosChoose (family CaptureSite) role reservedSite ordinarySite)) (naturalIsZero (naturalEqual (captureSiteStride (aosChoose (family CaptureSite) role reservedSite ordinarySite)) 1)))) (nativeTelemetrySourceScopeAdmission applicationBytes ordinaryCapacity reservedCapacity (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) resultSlot workSlot coordinate)))))) (nativeTelemetrySiteCommands applicationBytes policy (aosChoose (family CaptureSite) role reservedSite ordinarySite) ordinaryCapacity reservedCapacity ordinary reserved bound (aosChoose (family TelemetryRecordPlan) role reserved ordinary) values coordinate resultSlot workSlot identity tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail))) (branch TelemetryDrainRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))) (branch TelemetryPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))))))))))) def nativeTelemetryPolicyInitializeWithIdentity = (lambda unrestricted initialize : (pi unrestricted applicationBytes : Nat . (pi unrestricted ordinary : Nat . (pi unrestricted reserved : Nat . (pi unrestricted result : Nat . (pi unrestricted identity : Bytes . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))))) . (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted required : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (modelWord64FromNaturalTruncated (captureControlAt applicationBytes)) (modelWord64FromNaturalTruncated (bytes-length (captureInitialControl ordinaryCapacity reservedCapacity required))) (captureInitialControl ordinaryCapacity reservedCapacity required)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalCopyPayloadToState (modelWord64FromNaturalTruncated (publicationBase applicationBytes ordinaryCapacity reservedCapacity)) (modelWord64FromNaturalTruncated (bytes-length (dataBytesRepeatByte (byte 0) publicationStateBytes))) (dataBytesRepeatByte (byte 0) publicationStateBytes)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalStoreWord64 (nativeTelemetryPolicyState decisionAt) (nativeLaunchRecipeImmediate 4)) identity (initialize applicationBytes ordinaryCapacity reservedCapacity resultSlot identity tail))))))))))))) def nativeTelemetryPolicyInitializeWith = (nativeTelemetryPolicyInitializeWithIdentity nativeTelemetryIdentityCommand) def nativeTelemetryPolicyInitialize = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryPolicyPlan) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryPolicyPlan (lambda unrestricted current : (family TelemetryPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryPolicyReady policy ordinarySite reservedSite drain . (eliminate TelemetryDrainPlan (lambda unrestricted current : (family TelemetryDrainPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDrainReady ordinaryCapacity reservedCapacity ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (telemetryPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (nativeTelemetryPolicyInitializeWith applicationBytes ordinaryCapacity reservedCapacity (capturePolicyRequired policy) (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) resultSlot identity tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail))) (branch TelemetryDrainRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))) (branch TelemetryPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))))))) -- ABI: control, publication state, capture decision, terminal request, -- publication-result address, exact publication extent. Result address and -- buffers are admitted by the VM operand and arena owners. Return only 0/1. -- Seven means not requested, not a fabricated durability acknowledgement. -- Source opportunities are selected plus excluded deltas, not elapsed time. def nativeTelemetryPolicyFlushRoutine = (lambda unrestricted threshold : Nat . (lambda unrestricted bound : Nat . (compiler-native-encode (family X86NativeAssembly) (telemetryPolicyFlushAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) policyX86Backend threshold bound)))) -- Call at a declared safe boundary. Capture and publication outcomes stay -- separate. Pending values must be retried after a nonterminal acknowledgement; -- a terminal request while pending refuses to invent producer completion. def nativeTelemetryPolicyBoundaryWith = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted bound : Nat . (lambda unrestricted threshold : Nat . (lambda unrestricted decisionAt : Nat . (lambda unrestricted terminal : Nat . (lambda unrestricted captureSlot : Nat . (lambda unrestricted publicationSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted drain : (pi unrestricted commands : (family NativePhysicalCommands) . (family NativePhysicalCommands)) . (lambda unrestricted tail : (family NativePhysicalCommands) . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (nativeTelemetryPolicyFlushRoutine threshold bound) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeTelemetryPolicyState (captureControlAt applicationBytes)) (nativeTelemetryPolicyState (publicationBase applicationBytes ordinaryCapacity reservedCapacity)) (nativeLaunchRecipeSlotValue captureSlot) (nativeLaunchRecipeImmediate terminal) (nativeTelemetryPolicyState decisionAt) (nativeLaunchRecipeImmediate (publicationArenaBytesForBody bound))) (nativeLaunchRecipeStore workSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine recordStatusRoutine (nativeLaunchRecipeArguments (nativeTelemetryPolicyState decisionAt) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore publicationSlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue workSlot)) identity (drain (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity tail)))))))))))))))))) def nativeTelemetryPolicyBoundaryCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryPolicyPlan) . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted captureSlot : Nat . (lambda unrestricted publicationSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryPolicyPlan (lambda unrestricted current : (family TelemetryPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryPolicyReady policy ordinarySite reservedSite drain . (eliminate TelemetryDrainPlan (lambda unrestricted current : (family TelemetryDrainPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDrainReady ordinaryCapacity reservedCapacity ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (naturalAnd (naturalLessOrEqual terminal 1) (naturalAnd (naturalIsZero (naturalEqual captureSlot publicationSlot)) (naturalAnd (naturalIsZero (naturalEqual captureSlot workSlot)) (naturalAnd (naturalIsZero (naturalEqual publicationSlot workSlot)) (telemetryPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound))))) (nativeTelemetryPolicyBoundaryWith applicationBytes ordinaryCapacity reservedCapacity bound (capturePolicyFlushOpportunities policy) (telemetryPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) terminal captureSlot publicationSlot workSlot identity (nativeTelemetryDrainCommands applicationBytes drain terminal sink directory publicationSlot identity) tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail))) (branch TelemetryDrainRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail)))) (branch TelemetryPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (nativeLaunchRecipeArguments (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (constructor NativePhysicalResultBinding NativePhysicalDiscardResult)) identity tail))))))))))))) def nativeTelemetrySourceOutsideRegion = (lambda unrestricted regionAt : Nat . (lambda unrestricted regionBytes : Nat . (lambda unrestricted operand : (family NativePhysicalOperand) . (eliminate NativePhysicalOperand (lambda unrestricted current : (family NativePhysicalOperand) . Nat) operand (branch NativePhysicalImmediate value . 1) (branch NativePhysicalResultValue slot . 1) (branch NativePhysicalResultAddress slot offset . 1) (branch NativePhysicalStateAddress offset . 1) (branch NativePhysicalStateLoad64 offset . (naturalOr (naturalAnd (naturalLessOrEqual captureWordBytes regionAt) (naturalLessOrEqual (modelWord64Natural offset) (naturalSaturatingSubtract regionAt captureWordBytes))) (naturalLessOrEqual (naturalAdd regionAt regionBytes) (modelWord64Natural offset)))) (branch NativePhysicalPayloadAddress offset . 1) (branch NativePhysicalPayloadLoad64 offset . 1) (branch NativePhysicalProcessArgument index . 1) (branch NativePhysicalLoopAffine base stride . 1))))) def nativeTelemetryRoutedSourceScopeAdmission = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted ordinaryCapacity : Nat . (lambda unrestricted reservedCapacity : Nat . (lambda unrestricted ordinary : (family TelemetryRecordPlan) . (lambda unrestricted reserved : (family TelemetryRecordPlan) . (lambda unrestricted bound : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted operand : (family NativePhysicalOperand) . (naturalAnd (nativeTelemetrySourceScopeAdmission applicationBytes ordinaryCapacity reservedCapacity (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) resultSlot workSlot operand) (nativeTelemetrySourceOutsideRegion (telemetryDispatchTagsAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalSaturatingSubtract (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (telemetryDispatchTagsAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) operand))))))))))) def nativeTelemetryRoutedCaptureSiteCommand = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted wanted : Nat . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDispatchReady ordinaryCapacity reservedCapacity ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (family NativePhysicalCommands)) (telemetryPolicySiteLookup wanted sites) (branch TelemetryPolicySitesEnd . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)) (branch TelemetryPolicySitesNext tag site declaration following induction . (let unrestricted recipe = (telemetryRecordRouteLookup tag (aosChoose (family TelemetryRecordRoutes) (captureSiteReserved site) reservedRoutes ordinaryRoutes)) in (aosChoose (family NativePhysicalCommands) (naturalAnd (telemetryRoutedPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (naturalAnd (naturalIsZero (naturalEqual resultSlot workSlot)) (naturalAnd (naturalOr (naturalIsZero (captureSiteSelected policy site)) (naturalAnd (nativeTelemetrySourcesAdmission recipe values) (nativeTelemetrySourceScopesWith recipe values (nativeTelemetryRoutedSourceScopeAdmission applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound resultSlot workSlot)))) (naturalOr (naturalIsZero (naturalAnd (captureSiteSelected policy site) (naturalIsZero (naturalEqual (captureSiteStride site) 1)))) (nativeTelemetryRoutedSourceScopeAdmission applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound resultSlot workSlot coordinate))))) (nativeTelemetrySiteWith applicationBytes policy site ordinaryCapacity reservedCapacity bound (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) recipe values coordinate resultSlot workSlot identity (lambda unrestricted commands : (family NativePhysicalCommands) . (nativeTelemetryCaptureSelectedCommand applicationBytes ordinaryCapacity reservedCapacity (nativeTelemetryPolicyLoad (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (captureSiteReserved site) resultSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (drainCommitTagRoutine ordinaryCapacity reservedCapacity (captureSiteReserved site) tag) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeTelemetryPolicyState (captureControlAt applicationBytes)) (nativeTelemetryPolicyState (telemetryDispatchTagsAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound)) (nativeLaunchRecipeSlotValue resultSlot) (nativeLaunchRecipeImmediate (telemetryDispatchTagsBytes ordinaryCapacity reservedCapacity)) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity commands))) tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))))) (branch TelemetryDispatchRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))) (branch TelemetryRoutedPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))))))))))) def nativeTelemetryRoutedPolicyInitializeWithIdentity = (lambda unrestricted initialize : (pi unrestricted applicationBytes : Nat . (pi unrestricted ordinary : Nat . (pi unrestricted reserved : Nat . (pi unrestricted result : Nat . (pi unrestricted identity : Bytes . (pi unrestricted tail : (family NativePhysicalCommands) . (family NativePhysicalCommands))))))) . (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted resultSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDispatchReady ordinaryCapacity reservedCapacity ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (telemetryRoutedPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) (nativeTelemetryPolicyInitializeWithIdentity initialize applicationBytes ordinaryCapacity reservedCapacity (capturePolicyRequired policy) (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) resultSlot identity tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))) (branch TelemetryDispatchRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))) (branch TelemetryRoutedPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))))))))) def nativeTelemetryRoutedPolicyInitialize = (nativeTelemetryRoutedPolicyInitializeWithIdentity nativeTelemetryIdentityCommand) def nativeTelemetryRoutedPolicyBoundaryCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted terminal : Nat . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted captureSlot : Nat . (lambda unrestricted resultSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryDispatchPlan (lambda unrestricted current : (family TelemetryDispatchPlan) . (family NativePhysicalCommands)) drain (branch TelemetryDispatchReady ordinaryCapacity reservedCapacity ordinaryRoutes reservedRoutes ordinary reserved descriptors bound . (aosChoose (family NativePhysicalCommands) (naturalAnd (naturalLessOrEqual terminal 1) (naturalAnd (naturalAnd (naturalIsZero (naturalEqual resultSlot captureSlot)) (naturalAnd (naturalIsZero (naturalEqual resultSlot workSlot)) (naturalIsZero (naturalEqual captureSlot workSlot)))) (telemetryRoutedPolicyArenaCertificate applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound))) (nativeTelemetryPolicyBoundaryWith applicationBytes ordinaryCapacity reservedCapacity bound (capturePolicyFlushOpportunities policy) (telemetryRoutedPolicyDecisionAt applicationBytes ordinaryCapacity reservedCapacity ordinary reserved bound) terminal captureSlot resultSlot workSlot identity (nativeTelemetryDispatchDrainCommands applicationBytes drain terminal sink directory resultSlot identity) tail) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))) (branch TelemetryDispatchRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail)))) (branch TelemetryRoutedPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore resultSlot)) identity tail))))))))))))) def nativeTelemetryFailureIdentity = (lambda unrestricted name : Bytes . (bytes-append name (dataBytesRepeatByte (byte 0) (naturalSaturatingSubtract 64 (bytes-length name))))) def nativeTelemetryPendingRoutine = (compiler-native-encode (family X86NativeAssembly) (telemetryPolicyPendingAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) policyX86Backend)) def nativeTelemetryContinuationRoutine = (lambda unrestricted required : Nat . (compiler-native-encode (family X86NativeAssembly) (telemetryPolicyContinuationAssemblyFor (family X86NativeAssembly) (family X86NativeRegister64) policyX86Backend required))) -- One capture at a declared safe boundary. No caller operation can intervene -- between pending acquisition, durable drain and retry of the frozen values. -- Retry is bounded once; zero capacity or refusal fails by name. Optional -- accounted drops may continue; an inaccessible/poisoned sink may not silently -- run unobserved. This is not a concurrent writer or an asynchronous uploader. def nativeTelemetryRoutedCaptureAndContinueCommands = (lambda unrestricted applicationBytes : Nat . (lambda unrestricted plan : (family TelemetryRoutedPolicyPlan) . (lambda unrestricted wanted : Nat . (lambda unrestricted values : (family NativeTelemetrySourceValues) . (lambda unrestricted coordinate : (family NativePhysicalOperand) . (lambda unrestricted sink : (family NativePhysicalOperand) . (lambda unrestricted directory : (family NativePhysicalOperand) . (lambda unrestricted captureSlot : Nat . (lambda unrestricted publicationSlot : Nat . (lambda unrestricted workSlot : Nat . (lambda unrestricted retrySlot : Nat . (lambda unrestricted identity : Bytes . (lambda unrestricted tail : (family NativePhysicalCommands) . (eliminate TelemetryRoutedPolicyPlan (lambda unrestricted current : (family TelemetryRoutedPolicyPlan) . (family NativePhysicalCommands)) plan (branch TelemetryRoutedPolicyReady policy sites drain . (eliminate TelemetryPolicySites (lambda unrestricted current : (family TelemetryPolicySites) . (family NativePhysicalCommands)) (telemetryPolicySiteLookup wanted sites) (branch TelemetryPolicySitesEnd . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore captureSlot)) identity tail)) (branch TelemetryPolicySitesNext tag site declaration following induction . (aosChoose (family NativePhysicalCommands) (naturalAnd (naturalIsZero (naturalEqual workSlot retrySlot)) (naturalAnd (naturalIsZero (naturalEqual publicationSlot retrySlot)) (naturalAnd (naturalIsZero (naturalEqual publicationSlot workSlot)) (naturalAnd (naturalIsZero (naturalEqual captureSlot retrySlot)) (naturalAnd (naturalIsZero (naturalEqual captureSlot workSlot)) (naturalAnd (naturalIsZero (naturalEqual captureSlot publicationSlot)) 1)))))) (nativeTelemetryRoutedCaptureSiteCommand applicationBytes plan wanted values coordinate captureSlot workSlot identity (aosChoose (family NativePhysicalCommands) (captureSiteSelected policy site) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine nativeTelemetryPendingRoutine (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeSlotValue captureSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore retrySlot)) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatBeginCounted (nativeLaunchRecipeSlotValue retrySlot)) identity (nativeTelemetryRoutedPolicyBoundaryCommands applicationBytes plan 0 sink directory captureSlot publicationSlot workSlot identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue publicationSlot) (nativeLaunchRecipeImmediate 0) (nativeTelemetryFailureIdentity b"telemetry:pending-drain-refused") (nativeTelemetryDispatchCaptureCommand applicationBytes drain 1 (captureSiteReserved site) wanted captureSlot identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue captureSlot) (nativeLaunchRecipeImmediate 1) (nativeTelemetryFailureIdentity b"telemetry:pending-retry-refused") (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalRepeatEnd) identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (nativeTelemetryContinuationRoutine (capturePolicyRequired policy)) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeSlotValue captureSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore retrySlot)) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue retrySlot) (nativeLaunchRecipeImmediate 1) (nativeTelemetryFailureIdentity b"telemetry:capture-refused") (nativeTelemetryRoutedPolicyBoundaryCommands applicationBytes plan 0 sink directory captureSlot publicationSlot workSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalAssertOneOf (nativeLaunchRecipeSlotValue publicationSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 7) (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed)) (nativeTelemetryFailureIdentity b"telemetry:publication-refused") tail))))))))))) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine (nativeTelemetryContinuationRoutine (capturePolicyRequired policy)) (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeSlotValue captureSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore retrySlot)) identity (nativeLaunchRecipeAssertEqual (nativeLaunchRecipeSlotValue retrySlot) (nativeLaunchRecipeImmediate 1) (nativeTelemetryFailureIdentity b"telemetry:capture-refused") (nativeTelemetryRoutedPolicyBoundaryCommands applicationBytes plan 0 sink directory captureSlot publicationSlot workSlot identity (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalAssertOneOf (nativeLaunchRecipeSlotValue publicationSlot) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 7) (constructor NativePhysicalErrorCode NativePhysicalExecutionAssertionFailed)) (nativeTelemetryFailureIdentity b"telemetry:publication-refused") tail)))))) (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore captureSlot)) identity tail))))) (branch TelemetryRoutedPolicyRefused reason . (nativeLaunchRecipeCommand (constructor NativePhysicalOperation NativePhysicalMachineRoutine b"" (constructor NativePhysicalArguments NativePhysicalArgumentsValue (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0) (nativeLaunchRecipeImmediate 0)) (nativeLaunchRecipeStore captureSlot)) identity tail))))))))))))))))